Claude подготовил доказательства для кода из 123 библиотек

Anthropic и компания Theorem показали, как Claude может писать формальные доказательства для реального программного кода. В исследовании от 22 октября сообщается о проверке выбранных свойств 239 точек входа из 123 открытых библиотек. Результаты проверяет отдельная система Rocq. Это шаг к проверяемой работе ИИ в разработке, но он не означает, что все эти библиотеки теперь свободны от ошибок.

В чём новость: модель пишет, проверяющая система проверяет

Обычный ответ ИИ «я проверил код, проблем нет» остаётся текстовым утверждением. Формальная верификация устроена иначе: нужно точно описать свойство программы, а затем построить математическое доказательство того, что оно выполняется в заданной модели исполнения. В этой схеме Claude помогает создать доказательство, а его соответствие утверждению проверяется машинно.

Rocq — система разработки и проверки доказательств, раньше известная как Coq. Она позволяет формулировать спецификации, записывать теоремы и проверять доказательства небольшим ядром. Полагаться только на уверенность языковой модели в таком процессе не требуется. Но смысл выбранного утверждения и правильность исходных предположений по-прежнему имеют значение.

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

Как существующие тесты превратили в задачу для доказательства

Команда взяла точки входа из OSS-Fuzz — инфраструктуры тестирования открытого ПО. Фаззинг, или fuzzing, проверяет программу множеством автоматически полученных входных данных, чтобы найти ошибки. Этот подход хорошо ищет сбои, но успешное прохождение большого числа примеров само по себе не доказывает отсутствие проблемы на каждом возможном входе.

В проекте тестируемую программу компилировали в исполняемый файл RISC-V и описывали её поведение с помощью формальной модели процессора и Linux. Затем Claude строил доказательства заданных свойств. Если во время работы обнаруживалась ошибка исходного кода, агент мог предложить исправление, после чего проверка относилась уже к обновлённой программе.

По отчёту Anthropic, работа охватила 239 точек входа в 123 библиотеках. Важны слова «точки входа»: это выбранные пути, через которые тест подаёт данные в программу. Число библиотек не означает, что доказано всё поведение каждого проекта. Основной результат касается определённых исполняемых файлов, ограничений на входы и принятой модели окружения.

Что опубликовано и почему полезно открыть репозиторий

В открытом репозитории Theorem oss-verify-proofs размещена часть результатов: на момент проверки README перечисляет доказательства для 60 точек входа в 25 библиотеках. Это опубликованное подмножество большого исследования; его нельзя выдавать за все 239 результатов, о которых сообщает Anthropic.

Репозиторий описывает утверждения, версии компонентов и процедуру проверки. Указан Rocq 9.2.0, а свойства сформулированы в LPS — формальной модели процесса Linux, исполняющего RISC-V-код. Авторы отдельно перечисляют ограничения модели и компоненты, которым приходится доверять.

В этом и состоит практический интерес открытых артефактов: исследователь может рассматривать не только красивую диаграмму, но и само утверждение, сборку и правила проверки. Редакция изучила описание и ограничения; самостоятельно полный комплект доказательств не пересобирала. Доступность файлов не равна независимому воспроизведению всего эксперимента.

Три границы, которые нельзя потерять в заголовке

Авторы репозитория подчёркивают, что опубликованные доказательства относятся к конкретным статическим сборкам riscv64 с musl. Они не являются доказательствами для исходного текста вообще или для обычных x86-64-сборок OSS-Fuzz. Ошибки за пределами проверяемых свойств, например неверный результат вычисления, таким способом не исключаются.

Есть и отдельная тонкость: в описании открытого набора прямо сказано, что ни одно опубликованное доказательство не устанавливает обязательное завершение программы. Поэтому формулировка «Claude доказал, что эти программы всегда успешно завершаются» была бы шире доступного результата. Отсутствие определённого сбоя и доказанное завершение — разные свойства.

Почему это отличается от очередного рекорда модели

Интерес здесь вызывает сам рабочий процесс: языковая модель выполняет трудоёмкую подготовку, а результат можно проверять по формальным правилам. Это более содержательный критерий, чем субъективное «ответ выглядит убедительно». Однако польза зависит от того, правильно ли выбрано свойство и достаточно ли точно описано реальное окружение.

Представим функцию обработки файла. Можно искать вход, на котором она падает; можно проверить несколько заранее известных примеров; можно сформулировать ограниченное свойство и попытаться доказать его. Эти действия отвечают на разные вопросы. Их разумно сочетать: тесты показывают ожидаемое поведение на примерах, а доказательство даёт другой тип основания для доверия в пределах своей формулировки.

Для владельца сайта это не готовая кнопка «проверить WordPress». Исследовательская цепочка работает с определёнными бинарными программами, а не с любым PHP-плагином по ссылке. Перенос подхода в повседневную веб-разработку потребует подходящих инструментов и свойств, которые действительно отражают требования проекта.

Что разработчику можно взять из этой работы уже сейчас

Редакционный вывод — чаще просить от ИИ результат, который можно проверить независимо. Для обычной задачи это может быть воспроизводимый пример ошибки, тест с ожидаемым ответом, небольшой патч или перечень явно сформулированных условий. Формальное доказательство — более строгий инструмент для тех случаев, где есть подходящая спецификация и инфраструктура.

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

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

Новость продолжает тему проверки ответов нейросетей: доверие опирается на проверяемые основания. А в агентном процессе, где модель не только советует, но и меняет файлы, стоит отдельно контролировать границы задачи — об устройстве таких исполнителей писали в статье про агентов Claude Code.

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