ИИ удешевляет формальную верификацию кода: 20 человеко-лет работы сжимаются до дней

До сих пор формальная верификация стоила непропорционально дорого. Показательный пример из источника: микроядро seL4 содержало 8 700 строк кода на C, а доказательство его корректности потребовало 20 человеко-лет и 200 000 строк кода на языке Isabelle. Это 23 строки доказательства и половина рабочего дня специалиста на каждую строку исходного кода. Специалистов, способных писать такие доказательства, в мире считанные сотни. В экономических терминах: ожидаемая стоимость багов почти всегда была ниже стоимости их формального устранения, поэтому индустрия обходилась тестами.

Автор оригинального материала утверждает, что ИИ-агенты (автономные программы на базе LLM) уже умеют генерировать доказательные скрипты на нескольких языках и что в ближайшие годы процесс может быть полностью автоматизирован. Если это произойдёт, экономика формальной верификации изменится радикально.

Что понадобится для старта?

• Язык доказательств. Один из пяти основных: Lean, Isabelle, Rocq (ранее Coq), F* или Agda. Для новичка автор выделяет Lean как наиболее активно развивающийся
• LLM с доступом к коду. ChatGPT (GPT-4o), Claude от Anthropic или открытая модель (опенсорс) с поддержкой длинного контекста. Из доступных в РФ вариантов подойдут GigaChat или YandexGPT для простых задач, но для работы с доказательствами пока сильнее зарубежные модели
• Среда разработки. VS Code с расширением для выбранного языка доказательств (для Lean это lean4-mode или Lean extension)
• Время. На первый цикл «спецификация, генерация кода, проверка доказательства» заложите выходной день. Дальше каждая итерация будет занимать часы, а не недели

Пошаговая инструкция

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

2. Переведите спецификацию на формальный язык с помощью LLM. Отправьте промпт (текстовый запрос к модели) вида:

Переведи следующую спецификацию на язык Lean 4.
Функция sort принимает List Nat и возвращает List Nat.
Свойства:

- длина результата равна длине входа
- результат отсортирован по возрастанию
- каждый элемент входа присутствует в результате

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

2. Запросите доказательство. Отправьте следующий промпт:

Напиши доказательство на Lean 4, что функция sort
удовлетворяет спецификации sortSpec.
Если доказательство не проходит проверку,
объясни причину и предложи исправление.

1. Прогоните результат через проверщик доказательств (proof checker). Это небольшая программа, встроенная в Lean или Isabelle, которая математически верифицирует каждый шаг. Галлюцинация (когда ИИ уверенно выдумывает то, чего не было) здесь не страшна: проверщик отвергнет любое некорректное доказательство, и модели придётся пробовать снова

2. Итерируйте. Если проверщик отклонил доказательство, передайте ошибку обратно в LLM. Цикл «генерация, проверка, исправление» повторяется до тех пор, пока доказательство не пройдёт. Именно в этом цикле ИИ экономит месяцы ручной работы

Что делать с этим прямо сейчас, по ролям

Разработчику в РФ. Установите Lean 4, пройдите официальный учебник «Theorem Proving in Lean 4» (бесплатный, на английском, но LLM поможет с переводом). Начните с доказательства простых свойств маленьких функций. Через полгода этот навык перестанет быть экзотикой.

Автору Дзена, пишущему о технологиях. Термин «верикодинг» (vericoding, противопоставление вайб-кодингу) появился в сентябре 2025 года и обозначает применение LLM для генерации формально верифицированного кода. Это свежая тема с минимальной конкуренцией в русскоязычном поле.

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

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