Формальная верификация — метод доказательства корректности кода математическими средствами — десятилетиями оставалась уделом исследователей. Пример seL4, микроядра операционной системы, наглядно демонстрирует причины: 8 700 строк кода на C потребовали 200 000 строк доказательств на языке Isabelle и 20 человеко-лет работы. В переводе на экономику это означает, что стоимость доказательств превышает ожидаемую стоимость багов, которые они предотвращают. Поэтому в промышленности, даже в авиации и медицинском приборостроении, формальные методы применяются редко.
Автор прогноза, опубликованного на Habr, утверждает: ситуация изменится под влиянием ИИ. LLM-агенты, которые уже успешно генерируют код, начинают справляться и с написанием доказательных скриптов. Ключевое преимущество такого подхода — встроенная защита от галлюцинаций: механизм проверки доказательств отвергнет любое неверное утверждение, заставляя модель итерировать. Это делает доказательство корректности сгенерированного кода более надёжным, чем традиционная вычитка человеком.
Если верификация подешевеет, её можно будет применять к гораздо большему объёму софта. Причём потребность в ней растёт параллельно: чем больше кода пишут нейросети, тем острее необходимость доказывать его корректность. Автор предполагает, что в перспективе разработчик будет описывать спецификацию на высокоуровневом декларативном языке, а ИИ-агент — генерировать реализацию, удовлетворяющую доказательству. Самый сложный этап сместится с написания доказательств к формулировке спецификаций — что именно нужно доказать. Это требует опыта, но несравнимо легче, чем ручное доказательство.
Остаются открытые вопросы. Во-первых, формальные спецификации сами могут содержать ошибки — свойства, доказанные для кода, могут не совпадать с реальными требованиями. Во-вторых, перевод спецификаций на естественный язык и обратно потенциально теряет тонкости. Тем не менее, автор считает эти риски управляемыми. Показательно, что крупные верифицированные системы — ядро ОС, компилятор C, стек криптопротоколов — уже существуют, но их создание требовало усилий уровня PhD. ИИ может демократизировать этот процесс, сделав формальную верификацию стандартной практикой, а не экзотикой.
