Как ИИ превратит формальную верификацию в главный стандарт разработки ПО

Новое дыхание математического доказательства в программировании

Сегодня обсуждения вокруг искусственного интеллекта в IT-индустрии вращаются преимущественно вокруг генерации стандартного кода и автодополнения. Однако я обращаю внимание на другой критически важный аспект, который долгое время оставался в тени. Нейросети способны вывести математически строгую формальную верификацию из узкой академической ниши непосредственно в массовую практику инженерии программного обеспечения.

В распоряжении специалистов уже не один год есть специализированные языки и системы для построения формальных доказательств — в их числе Rocq, Isabelle, Lean, F* и Agda. Их задача заключается в том, чтобы зафиксировать строго детерминированные требования к поведению системы в виде спецификаций, а затем математическим путем подтвердить, что разработанный код безукоризненно выполняет эти правила. Такой подход гарантирует отсутствие сбоев даже в самых необычных краевых сценариях, о которых разработчик мог даже не задумываться на этапе тестирования.

Подобные инструменты ранее находили применение лишь при создании фундаментальных систем с максимальными требованиями к надежности. В качестве примеров можно назвать верифицированные ядра операционных систем, специализированные компиляторы для языка C и криптографические протокольные стеки.

Почему формальные методы оставались академической экзотикой

Несмотря на колоссальные преимущества в надежности, коммерческая разработка софта практически полностью игнорировала формальную верификацию. Даже в отраслях с невероятно высокой ответственностью — например, в медицинской технике или авиационном ПО — инженерные команды крайне редко применяли математическое доказательство корректности. Причина кроется в колоссальной сложности процесса: от специалистов требовалась подготовка уровня доктора наук и колоссальные временные затраты.

Яркой иллюстрацией этой проблемы служат показатели проекта микроядра seL4. По данным на 2009 год, реализация самого ядра на языке C занимала порядка 8 700 строк. Однако чтобы математически доказать полную корректность этого объема, потребовалось написать свыше 200 000 строк доказательного кода на языке Isabelle, а общий объем затраченного времени составил около 20 человеко-лет. В пересчете на объем получается, что одна строка C-кода требовала около 23 строк доказательств и примерно половины рабочего дня одного высококлассного эксперта. Учитывая, что специалистов с подобными специфическими знаниями в мире исчислялось в лучшем случае несколькими сотнями, массовое применение метода было невозможно.

С точки зрения экономики ситуация выглядела прозрачно: финансовый риск от вероятных ошибок в большинстве программ был существенно ниже, чем огромная стоимость привлечения математиков для написания доказательных скриптов. Дополнительно сказывалось то, что убытки от сбоев чаще перекладывались на конечных пользователей, а не на самих создателей софта. Но даже при желании разработчиков снизить риски издержки на верификацию оставались неподъемными.

LLM и перелом в экономике разработки

Внедрение языковых моделей и специализированных ИИ-агентов кардинально меняет сложившийся порядок. Выяснилось, что нейросети способны успешно справляться не только с написанием исполняемого кода, но и с генерацией доказательных скриптов для специализированных языков верификации. Хотя на текущем этапе процессом всё еще руководит опытный программист, динамика развития технологий показывает, что полная автоматизация этого этапа — вопрос ближайших лет.

Если процесс доказательства подешевеет на порядки, экономическая целесообразность формальной верификации изменится до узнаваемости. Мы сможем гарантировать абсолютную надежность для софта любого уровня. Более того, само распространение генеративного ИИ создает острый запрос на такую проверку: вместо того чтобы тратить часы человеческого времени на вычитку сгенерированных нейросетью алгоритмов, гораздо логичнее поручить ИИ доказать корректность собственной работы.

Написание скриптов доказательств можно назвать одной из самых идеальных сфер применения больших языковых моделей. Дело в том, что свойственная LLM проблема галлюцинаций здесь полностью нейтрализуется. Написанное предложение сразу отправляется в детерминированный механизм проверки доказательств (proof checker). Если алгоритм найдет в доказательстве ошибку, он мгновенно отвергнет его и заставит нейросеть сформировать новый вариант. Сам проверяющий модуль представляет собой компактную, формально верифицированную программу, что исключает ложные срабатывания.

От проверки кода к согласованию спецификаций: концепция «верикодинга»

Автоматизация не ликвидирует баги полностью, но смещает главную сложность разработки. Фокус внимания инженеров сместится с рутинной реализации на составление правильных спецификаций. Ключевой задачей станет точное формулирование того, какими именно свойствами должен обладать программный модуль.

Составление спецификаций всё так же потребует от специалиста высокого уровня погружения и логического мышления, но написать декларативные требования несоизмеримо проще и быстрее, чем ручным трудом выстраивать доказательную базу. В дальнейшем ИИ-агенты смогут оказывать помощь и на этом участке — переводя требования с естественного языка на формальный и обратно для удобства проверки human-in-the-loop.

В перспективе такой подход формирует совершенно новую парадигму взаимодействия с софтом. Нам достаточно описать желаемое поведение на декларативном уровне высокого уровня, после чего нейросеть сгенерирует код реализации и сразу же подтвердит его корректность строгим доказательством. Нам не придется лично изучать машинные структуры сгенерированного ИИ кода — точно так же, как современные программисты не вычитывают ассемблерный код, создаваемый компилятором.

В научной публикации от сентября 2025 года для описания данного процесса был официально предложен термин «верикодинг» (vericoding) в противоположность хаотичному «вайб-кодингу». Верикодинг подразумевает совмещение скорости ИИ-генерации со строгим математическим контролем качества. В этом направлении уже активно работают стартапы и создаются специализированные нейросетевые модели, такие как Aristotle от Harmonic, Logical Intelligence и DeepSeek-Prover-V2. Главные достижения на данный момент сосредоточены вокруг экосистемы языка Lean.

Главным сдерживающим фактором на пути к массовому верикодингу станет не технологический барьер, а сдвиг в инженерной культуре. Разработчикам предстоит осознать, что формальные методы перестали быть теоретической концепцией и превратились в доступный рабочий инструмент.

Боты на серверах Telegram уже доступны — подайте заявку в бету

Помимо развития нейросетевых технологий для разработки, происходят изменения и в инфраструктуре популярных платформ. Разработчики Telegram начали предоставлять доступ к запуску ботов непосредственно на мощностях мессенджера. Это избавляет от необходимости арендовать сторонние VPS, разворачивать Docker-контейнеры, настраивать вебхуки и следить за непрерывным аптаймом серверов.

По сообщениям участников профильного сообщества @boto_shop, бета-тестирование серверного размещения ботов внутри инфраструктуры Telegram уже открыто для части пользователей, а подать заявку на участие в программе тестирования можно через специализированную форму.

Источник: habr.com