Claude доказал, что 123 библиотеки не падают: формальная верификация с ИИ

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

Взяли библиотеки из OSS-Fuzz — проекта Google, где популярные open-source библиотеки круглосуточно гоняются фаззерами. У каждой там уже есть точки входа для фазз-тестов. Их скомпилировали в статические бинарники под RISC-V с musl libc; медианный размер — около 18 тысяч машинных инструкций. Для каждой точки входа сформулировали теорему: программа не падает на любом входе меньше 64 МБ при любом смоделированном ответе Linux и любой раскладке памяти. «Падение» означает ошибку памяти по меркам AddressSanitizer или сработавший assert.

Доказательство пишет Claude, а проверяет его ядро Rocq — системы доказательств, которая раньше называлась Coq. Это ключевая деталь: модели не нужно верить на слово. Если в доказательстве есть ошибка, Rocq его просто не примет, как бы убедительно оно ни выглядело. За несколько недель так набралось около 180 миллионов строк доказательств на Rocq.

В русскоязычных пересказах исследования встречается утверждение, что «в основном использовался Verus для Rust». Это не так. Verus — верификатор для исходного кода на Rust, и машинный код он проверять не умеет. Главный результат про 123 библиотеки получен на RISC-V с доказательствами на Rocq.

Verus в работе тоже есть, но в отдельном примере: Claude написал интерпретатор Python на Rust и с помощью Verus доказал, что тот следует семантике CPython из академической статьи. На 1,7 миллиона случайных программ его поведение совпало с CPython в 99,95% тестов. x86 появляется в другом примере: Claude напрямую доказал, что скомпилированная под x86 реализация zlib из ядра Linux соответствует стандарту RFC 1950. Для этого он сам построил формальную семантику x86 и тщательно её протестировал.

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

Цена такого подхода — объём. Машинный код намного длиннее исходника, и доказательство про него тоже длинное: типичное занимает около 600 тысяч строк Rocq. Человек такое писать не стал бы. Модель может — и именно поэтому подход стал реальным только сейчас.

Попытки доказать спецификации выявили сотни багов. Если доказательство не сходится, причиной часто оказывается настоящая ошибка в коде. Тогда Claude исправлял её, спецификацию строили заново по исправленному коду, и доказательство продолжалось. Среди находок — переполнение счётчика вниз, чтение и запись за границами буфера, повторное открытие уязвимости CVE-2026-56132 в libexpat на глубоко вложенном входе и логическая ошибка, при которой ограничение на загрузку файлов срабатывало не всегда. Один баг пролежал в коде больше десяти лет.

Часть этих багов фаззеры почти не находят. Для одних нужен вход размером около 20 или 64 МБ, для других — больше 2 ГБ памяти или определённая последовательность вызовов. Это и есть главное отличие доказательства от тестирования: тест проверяет примеры, а доказательство — всё множество входов в заданных пределах. В отдельном опыте с читалкой PDF за неделю нашли столько уязвимостей, сколько обычно сообщают за год.

Отдельный риск — подмена задачи. Claude мог бы сделать любую теорему доказуемой, переписав программу так, чтобы она тривиально никогда не падала. Чтобы этого не случилось, любые патчи штрафовались, за доказательство того, какие входы патч меняет и как их мало, давали дополнительные баллы, а все исправления логировались и проверялись. Это тот же класс проблем, что и в разборах alignment: модель оптимизирует формальный критерий, и обвязка должна следить, чтобы она не обошла его в букве.

Классический пример цены — микроядро seL4, первое ядро ОС с полным машинно проверенным доказательством корректности (2009). Само ядро — около 8 700 строк C и 600 строк ассемблера — написали примерно за 2,2 человеко-года. Доказательство заняло около 200 тысяч строк в Isabelle и порядка 20 человеко-лет вместе с инструментами и исследованиями, из них около 11 — на доказательство самого seL4. Anthropic в своей публикации округляет это до «два года на ядро и двадцать на доказательство».

Поворот предсказывали. В декабре 2025 года Мартин Клеппман, автор книги «Высоконагруженные приложения», написал, что ИИ сделает формальную верификацию массовой. Его довод: главный барьер — цена доказательства, а у доказательства есть уникальное свойство: проверяющая программа отбрасывает правдоподобные, но ошибочные рассуждения. Значит, работу можно отдать модели, которая иногда ошибается, а доверять проверяющему. Публикация Anthropic — первое крупное подтверждение этого прогноза на реальном коде.

Пока это дорого: одно доказательство может стоить сотни миллионов токенов. Но динамика понятна. На бенчмарке из 36 задач на коде OSS-Fuzz Claude Opus 5.5 доказывает половину задач, тратя примерно на 40% меньше токенов, чем Opus 5. Когда несколько агентов работают с общим хранилищем доказательств и переиспользуют леммы друг друга, им нужно на 17% меньше токенов, а два доказательства в одиночку агенты не осилили вовсе.

Авторы прямо пишут: «формально проверено» не значит «без багов». Доказательство верно ровно настолько, насколько верны слои, на которые оно опирается. Нужно доверять формулировке теоремы, семантике RISC-V и процесса Linux, которую построила Theorem, ядру Rocq, а под ним — компилятору OCaml, операционной системе и железу. Если реальная машина делает то, чего нет в модели, доказательство об этом промолчит.

Есть и границы самого утверждения. Доказательства касаются однопоточных статических бинарников RISC-V с musl, а большинство людей запускает эти библиотеки на x86 или ARM с glibc и динамической линковкой. AddressSanitizer ловит не все ошибки памяти. Доказаны конкретные точки входа, а не вся библиотека. Вызывающий код, который использует библиотеку неправильно, всё ещё может испортить память — чтобы закрыть этот пробел, нужны обязательства для каждой функции, то есть предусловия.

Самый интересный вывод для обычного разработчика касается не RISC-V, а того, как писать код. Ещё в 1992 году Бертран Мейер описал контрактное программирование (Design by Contract): у функции есть предусловия — что должен гарантировать вызывающий, постусловия — что гарантирует сама функция, и инварианты — что остаётся истинным всё время. Мейер встроил контракты в язык Eiffel. Позже появились Dafny, где верификатор проверяет код прямо во время набора, и Verus для Rust.

Контракт — это и есть спецификация, которую можно доказывать. Когда инварианты записаны явно и формально, задача модели меняется: вместо «проверь, что код правильный» она получает чёткое утверждение, которое можно доказать или опровергнуть, а проверяющая программа подтвердит результат. Чем формальнее контракт, тем ближе рассуждение модели к настоящему доказательству. Вот так выглядит контракт в Verus:

Здесь три строки ensures — постусловия. Verus доказывает их для всех возможных пар a и b, а не для десятка примеров из теста. Если по ошибке написать a <= b вместо a >= b, функция начнёт возвращать меньшее число, проверка не пройдёт и покажет, какое условие нарушено.

Важная оговорка к популярному тезису «теперь код не тестируют, а доказывают». Сама Anthropic так не утверждает. Точки входа взяты из фазз-тестов, «падение» определено через AddressSanitizer, а собственную семантику x86 модель тщательно тестировала. Рассуждение модели об инвариантах без проверяющей программы — это не доказательство, а правдоподобная аргументация, которая может ошибаться. Сила подхода именно в связке: модель пишет, машина проверяет. Тесты при этом остаются нужны, потому что спецификация сама может быть неверной.

Theorem открыла сервис oss-verify: для подходящих open-source проектов он бесплатен, требует статических бинарников riscv64 и доказывает отсутствие падений на любом входе до 64 МиБ. Прогон может занять несколько дней. Доказательства из публикации, семантика RISC-V и процесса Linux и навык для Claude, который помогает добавить свой проект, выложены на GitHub. Для собственного кода порог входа ниже, чем кажется: Verus и Dafny работают локально, а писать контракты и доказательства к ним можно вместе с Claude Opus 5.5 через API Kumo.