Сейчас много говорят о том, как ИИ повлияет на разработку ПО, но есть такой ракурс, под которым проблему почти не рассматривают. Думаю, ИИ превратит в программно-инженерный мейнстрим формальную верификацию, которая десятилетиями развивалась где-то на периферии.
Уже довольно давно существуют языки программирования для программирования на основе доказательств, а также упрощающие такие доказательства — например, Rocq, Isabelle, Lean, F* и Agda. Они позволяют строго формализовать требования, которым должен удовлетворять определённый фрагмент кода, а затем математически доказать, что этот код всегда удовлетворяет этой спецификации (даже в странных изолированных случаях, которые вы и не подумали протестировать). При помощи этих инструментов уже давно разрабатывается ряд крупных и формально верифицированных программных систем, в числе которых — ядро операционной системы, компилятор для языка C и стек криптографических протоколов.
В настоящее время формальная верификация используется в основном в исследовательских проектах. Программисты, занятые в промышленности, очень редко пользуются формальными методами (речь даже о тех, кто разрабатывает классический софт с высокой планкой гарантий, например, в области медицинского приборостроения или авиации). Дело в том, что писать такие доказательства одновременно очень сложно (требуется подготовка на уровне кандидата наук) и очень трудоёмко.
Например, по состоянию на 2009 год в формально верифицированном микроядре seL4 было 8 700 строк кода на C. Но на доказательство его полной корректности потребовалось 20 человеко-лет и 200 000 строк кода Isabelle. Получается 23-строчное доказательство и половина рабочего дня одного специалиста на реализацию каждой строки рассматриваемого кода. Более того, в мире найдутся считанные сотни людей (кто знает?), умеющих писать такие доказательства, поскольку для этой работы требуется масса тайных знаний о системе доказательств.
То же самое формулируется на языке экономики так: в большинстве систем ожидаемая стоимость багов ниже ожидаемой стоимости тех доказательных приёмов, которые нужны для устранения этих багов. Отчасти ситуация обусловлена, пожалуй, и тем, что издержки от багов ложатся не на разработчика, а на пользователей (отрицательный внешний эффект). Но, если бы издержки даже нёс разработчик, формальная верификация банально очень сложна и дорого стоит.
Как минимум, именно так и обстояли дела до недавнего времени. Теперь программировать нам помогают агенты, основанные на LLM, преуспевающие не только в создании кода реализаций, но и в написании доказательных скриптов на разных языках. В настоящее время по-прежнему необходимо, чтобы рабочим процессом руководил человек-эксперт, но не сложно себе представить (экстраполировать), что в ближайшие несколько лет такие процессы будут полностью автоматизированы. Если это произойдёт, то экономика формальной верификации коренным образом изменится.
Если формальная верификация сильно подешевеет, то можно будет позволить себе верифицировать гораздо больше софта. Более того, ИИ также порождает потребность формально верифицировать гораздо больше софта. Чем заставлять людей вычитывать код, сгенерированный ИИ, я бы поручил ИИ доказать, что сгенерированный им код действительно корректен. Если бы это было возможно, то я везде и всегда предпочитал бы сгенерированный код рукописному (в котором найдётся сколько угодно кустарных багов)!
На самом деле, берусь утверждать, что написание доказательных скриптов — одна из самых полезных возможностей для применения LLM. В данном случае не важно, нагенерирует ли сеть галлюцинации, поскольку механизм проверки доказательств отвергнет любые неверные доказательства, принуждая ИИ пытаться снова и снова. Такой механизм — это небольшой объём кода, который также верифицирован, поэтому практически исключено, чтобы он пропустил некое некорректное доказательство.
Это не означает, что в программах вдруг исчезнут баги. По мере автоматизации процесса как такового самый сложный участок работы сместится в сторону того, как правильно описать спецификацию. То есть, откуда вам знать, что те свойства, которые были доказаны — именно те, что вас интересуют? Чтобы читать и писать такие формальные спецификации, всё равно потребуется как опыт, так и умение всё продумывать. Но написать спецификацию несравнимо легче и быстрее, чем вручную её доказывать, в этом и есть прогресс.
Также могу себе представить, как ИИ-агенты помогают писать спецификации и переводить с формального языка на естественный. При таком переводе тонкости потенциально могут потеряться, но кажется, что с такими рисками можно справиться.
Меня воодушевляет идея, что в спецификации на высокоуровневом декларативном языке можно попросту описать, какие свойства мы хотим получить в некотором фрагменте кода, а затем навайбкодить соответствующую реализацию, так, чтобы она удовлетворяла доказательству, написанному для данной спецификации. В результате процесс программирования принципиально изменится. Нам не потребуется даже заглядывать в код, сгенерированный ИИ, точно как сейчас мы не смотрим в машинный код, сгенерированный компилятором.
В качестве резюме: 1. Формальная верификация вот-вот принципиально подешевеет; 2. Код, сгенерированный ИИ, подлежит формальной верификации; таким образом, его можно будет не отдавать на ревью человеку, но быть уверенным, что этот код работает; 3. Строгость формальной верификации компенсирует неточность и вероятностную природу LLM. С учётом трёх этих обстоятельств в совокупности имеем, что в обозримом будущем формальная верификация, вероятно, станет мейнстримом. Подозреваю, что ограничивающим фактором здесь станут не технологии, а культурные сдвиги. Людям требуется осознать, что формальные методы уже жизнеспособны на практике.
Уточнения:
В этой статье от сентября 2025 года предложен термин «верикодинг» (противопоставляемый вайб-кодингу). Под верикодингом понимается применение LLM для генерации формально верифицированного кода, а также приводятся результаты бенчмаркинга по нескольких языках.
Эту отрасль развивают несколько стартапов: я слышал, что Aristotle от Harmonic , Logical Intelligence и DeepSeek-Prover-V2 уже довольно хорошо справляются с написанием гибких доказательств. На самом деле, кажется, что основные события разворачиваются именно в области Lean.