Статья Sid Trehan из Keller AI, вышедшая 10 ноября 2026, разбирает, что формальная верификация кода, написанного ИИ, доказывает на самом деле: подтверждается лишь соответствие кода конкретной математической спецификации при заявленных допущениях, а не «код без багов». На этом фоне она рассматривает два свежих примера — около 180 млн строк доказательств в Rocq, сгенерированных на Claude силами Anthropic и Theorem Labs, и прототип PDD Kit от GitHub Next и Microsoft Research, встраивающий верификатор Verus в цикл разработки. Ключевой вывод: ценность смещается от факта «доказательства» к качеству спецификации и списку допущений, которые теперь нужно ревьюить вручную.
Что произошло
Событие — публикация 10 ноября 2026 материала «AI proved your code correct. What did it actually prove?» автора Sid Trehan из компании Keller AI. Тезис статьи: проверка верификатором подтверждает соответствие кода конкретной математической спецификации при заявленных допущениях, но не гарантирует, что спецификация совпадает с бизнес-требованиями, и не покрывает немоделируемые эффекты вроде тайминг-атак. В качестве опорных примеров приведены две свежие работы. Первая — результат Anthropic совместно с Theorem Labs: на Claude сгенерировали около 180 млн строк доказательств в Rocq и доказали отсутствие падений (crash-freedom) для 239 точек входа в 123 библиотеках OSS-Fuzz на архитектуре RISC-V при входах до 64 МБ; попутно нашлись сотни багов, включая логический баг, просуществовавший более 10 лет. Вторая — прототип PDD Kit, выпущенный 2 ноября 2026 GitHub Next совместно с Microsoft Research: человек ревьюит намерение, агент пишет Rust-код, а верификатор Verus проверяет его.
Контекст
Формальная верификация десятилетиями оставалась нишей критических систем: по данным статьи, seL4 требовал около 20 человеко-лет на верификацию, а сами инструменты Rocq/Coq и seL4 существуют давно. Новизна текущего момента не в теории, а в экономике: LLM как синтезатор доказательств сокращает производство машино-проверяемых артефактов с человеко-лет до недель, то есть это scaling-результат по стоимости верификации, а не новый алгоритм проверки. Технически важно, что доказательства в Rocq проверяются ядром доказателя, поэтому вердикт бинарный — «принято или не принято» — и почти не поддаётся накрутке. Отсюда главный процессуальный сдвиг: ревью смещается с построчного чтения кода к проверке спецификации и допущений, а «зелёная галочка» верификатора сама начинает требовать аудита, иначе возникает «vibe verification» с тривиальными инвариантами.
Почему это важно для индустрии
Для индустрии это переход верификации из ниши критических систем в штатный этап пайплайна: агент пишет и код, и доказательства, Verus-проверки встраиваются в CI для Rust-компонентов, а формальная гарантия перестаёт быть ручной экспертизой единичных проектов. Для разработчиков продуктов и стартапов это прежде всего смена структуры затрат и модели доверия к агентно-сгенерированному коду: ценность смещается от факта наличия доказательства к качеству спецификации и доверенной базе допущений, поэтому в code review для генеративных пайплайнов становится обязательным аудит спек и допущений. В горизонте полугода логично ожидать независимого воспроизведения результата Anthropic сторонними командами, первых verifier-гейтов в CI агентных пайплайнов и бенчмарков качества спецификаций — именно они покажут, устойчив ли тренд. В горизонте пары лет возможна нормализация proof-driven development для критичных сегментов вроде парсеров, сериализации и криптодесериализации, а навыки ревью сместятся к формулированию спек и аудиту допущений.
Почему это важно для пользователей
Читателю, который применяет ИИ-агентов для кода, важно понимать, что означает фраза «агент доказал корректность»: доказано конкретное свойство, например crash-freedom, при конкретных допущениях — однопоточность, архитектура RISC-V, входы до 64 МБ — а не отсутствие любых багов. Практический вывод: вместо доверия к статусу проверки читать спецификацию и список trusted assumptions; в PDD Kit для этого предусмотрены sign-off cards на каждый внешний компонент, включая SQLite, bcrypt и JWT. Статья Keller AI интерактивная: в ней можно вручную собрать доказательство и увидеть, чем индукция отличается от тестов. Этот подход работает и вне прототипа: ревью намерения, спеки и списка допущений перед запуском агента даёт более честную гарантию, чем слепая вера в зелёную галочку верификатора.
Что пока неизвестно / ограничения
Результат Anthropic и Theorem Labs пока подтверждён единственным отчётом без публичного независимого репликативного прогона; вопрос открытости исходников доказательств для независимой перепроверки остаётся открытым. PDD Kit — прототип, и условия доступа по источникам неясны; отчёт Anthropic, со своей стороны, не сопровождается API, прайсингом или цифрами латентности. Сигналы очень свежие: PDD Kit вышел 2 ноября 2026, статья — 10 ноября 2026, поэтому коммерческих продуктов с ценами и SLA ещё нет. Домен пока узкий — в основном Rust с Verus и архитектура RISC-V, промышленное покрытие всего кода остаётся гипотетическим. Принципиальные пределы сохраняются: совпадение спецификации с бизнес-требованиями и немоделируемые эффекты вроде тайминг-атак остаются человеческой задачей и вне гарантий верификатора.
Источники
- AI proved your code correct. What did it actually prove? — Keller AI (Sid Trehan)
- LLMs are making formal software verification feasible at a much larger scale — Anthropic Research (совместно с Theorem Labs)
- PDD Kit — GitHub Next (совместно с Microsoft Research)
Автор
Look at AI, редакция