Инженеры снова заинтересовались формальной верификацией софта. Это может показаться удивительным: долгое время верификацию считали полезной лишь в узких нишевых случаях — в лучшем случае, а в худшем и вовсе бесполезной тратой времени. Тем не менее ажиотаж налицо: Google Trends показывает резкий всплеск запросов по темам formal verification и formal methods за последние два года, все вокруг изучают Lean, регулярно появляются новые языки спецификаций, а некоторые команды пытаются верифицировать крупные приложения целиком, от начала до конца (пример — проект Signal Shot).

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

Уилл Уилсон из Antithesis объявил победу этого традиционно нишевого направления в докладе We won, what now? — открывающем выступлении на Bug Bash 2026. Доклад получился содержательным и предлагает неплохие идеи о том, куда двигаться сообществу верификации теперь, когда тема стала мейнстримом.

На фоне этой «победы» любопытно вернуться к одной из классических статей против формальной верификации — Social Processes and Proofs of Theorems and Programs. В 1979 году её авторы писали:

«Мы полагаем, что (…) верификация программ обречена на провал. Мы не видим, каким образом она сможет повлиять на уверенность людей в корректности программ»

Ниже разбираются аргументы из этой статьи и проверяется, что из недавних изменений (если вообще что-то) их опровергает. Это скорее развлекательное упражнение, чем строго научное: статья на самом деле не утверждает, что обречены все усилия в области формальных методов — только полная верификация. Более того, далеко не очевидно, что верификация станет обычной частью разработки софта — пока видны лишь первые признаки интереса. Тем не менее переосмысление в 2026 году препятствий, которые 50 лет назад считались фундаментальными, кажется полезным и интересным занятием.

Аргумент 1: Математические доказательства — это социальные процессы

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

Комментарий

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

Аргумент 2: Проблемы со спецификацией

Первая часть аргумента звучит так: существует некое реальное, неформальное требование (у всех вовлечённых есть общее интуитивное понимание того, в чём оно состоит). Это интуитивное неформальное требование нужно перевести в формальную спецификацию — а сам процесс перевода неформален. В нём, никем не проверяемом, легко что-то потерять или неправильно истолковать.

Комментарий

Справедливое замечание. Контраргумент состоит в том, что спецификации ближе к неформальным требованиям, чем реализации — а значит, ошибку в них проще заметить. Кроме того, современные языки спецификаций (такие как Quint) позволяют интерактивно исследовать спецификацию и все её граничные случаи, чтобы убедиться, что она действительно соответствует изначальному замыслу.

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

Комментарий

Этот аргумент не выглядел сильным даже в прошлом, а тем более не выглядит таковым сейчас, когда в цикл разработки включены коддинг-агенты. Любое дополнительное понимание, полученное в процессе, в целом полезно для разработки. Люди, как финальные арбитры, решают, в какую сторону менять спецификацию, пересматривая исходные допущения. Коддинг-агентам можно доверить писать и менять код, а также создавать доказательства. Но если требуется изменить саму спецификацию, сделать это может только человек как финальный арбитр того, что значит «корректно» — а это возвращает к первой части аргумента 2.

Аргумент 3: Полностью автоматическая верификация недостижима

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

Комментарий

За прошедшее время в разработке автоматических верификаторов произошёл определённый прогресс, хотя человеческие усилия — написание доказательств или подходящей модели для model checking — по-прежнему остаются критически важными. Однако инструменты на базе LLM быстро сокращают этот разрыв. Игорь Коннов в посте Formal proofs for distributed protocols with AI may be closer than you think описывает опыт доказательства безопасности протокола Ben-Or в Lean.

Аргумент 4: Даже если бы полностью автоматическая верификация была достижима, она бы навредила

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

Комментарий

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

Аргумент 5: Реальные системы слишком запутаны, чтобы их можно было специфицировать

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

Комментарий

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

  • По мере проникновения софта в критическую инфраструктуру и мир финансов ставки растут.
  • Если есть надежда на то, что коддинг-агент создаст именно то, что нужно, стоит лучше уметь описывать, что именно нужно. Разумеется, это не всегда требует формальной спецификации, но искусство точно формулировать намерение становится важнее при работе с коддинг-агентами. Это не подразумевает полной верификации, но искусство спецификации — тоже один из инструментов формальных методов.

Аргумент 6: Надёжность софта — это гораздо больше, чем верификация

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

Комментарий

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

Заключение

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

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

Автор благодарит двух коллег по формальным методам, Томаса Пани и Ранадипа Бисваса, за полезные обсуждения статьи и этого материала. Было бы интересно услышать мнение людей вне этого «пузыря», которые по-прежнему считают формальные методы бесполезными.