Формальная верификация неожиданно стала мейнстримом. Google Trends показывает резкий скачок запросов за последние два года, все учат Lean, появляются новые языки спецификаций, а проект Signal Shot проверяет крупные приложения целиком. Драйвер — AI-кодинг: агенты оставляют код, который никто до конца не понимает, а инструменты верификации с LLM становятся быстрее и доступнее. Уилл Уилсон из Antithesis на открытии Bug Bash 2026 объявил победу направления.
В этой атмосфере интересно вернуться к статье 1979 года Social Processes and Proofs of Theorems and Programs. Её авторы утверждали, что верификация программ обречена и не сможет повлиять на доверие к коду. Правда, речь шла о полной верификации, а не обо всех формальных методах, да и неясно, станут ли они рутиной.
Первый аргумент: математические доказательства — это социальный процесс, а не механическая проверка. Возразить тут нечего: программам не обязательно повторять путь математики. Второй: неформальные требования приходится переводить в формальную спецификацию, и в этом переводе теряется смысл. Контраргумент: спецификации всё равно ближе к требованиям, чем код, а современные языки вроде Quint позволяют интерактивно посмотреть все крайние случаи. А вот потеря независимости спецификации от реализации в эпоху агентов — не проблема: человек остаётся финальным арбитром и решает, когда менять спецификацию.
Третий аргумент: полностью автоматическая верификация недостижима. С тех пор автоматические верификаторы продвинулись, но без человека всё ещё не обойтись. Однако LLM быстро закрывают разрыв: Игорь Коннов в посте Formal proofs for distributed protocols with AI may be closer than you think рассказал, как проверял безопасность протокола Ben-Or в Lean. Четвёртый: даже если верификация станет автоматической, она навредит — люди перестанут понимать программу. Это слабый довод, построенный на худших допущениях.
Пятый: реальные системы слишком грязные для спецификаций. Не всё нужно верифицировать, но софт всё глубже проникает в критическую инфраструктуру и финансы, ставки растут. А с AI-агентами умение точно описать желаемое становится критичным. Шестой: надёжность — это не только верификация. Здесь спорить не о чем: полная верификация не обязательна, но эти подходы не конкурируют, а дополняют друг друга.
Итог: статья была права, что формальная верификация — не панацея. Но её авторы напрасно списали со счетов отдельные инструменты формальных методов. С AI-агентами, которые пишут код, верификация особенно полезна: она замыкает контур и показывает агенту, тот ли код он написал.