Anthropic и компания Theorem показали, как большие языковые модели можно использовать не только для поиска ошибок, но и для формального доказательства отдельных свойств программ. В опубликованной 22 октября работе Claude подготовил доказательства для 239 тестовых точек входа в 123 библиотеках из проекта OSS-Fuzz.
Формальная верификация отличается от обычного тестирования: вместо перебора множества примеров создаётся математическое утверждение о поведении программы, а специальный проверяющий механизм подтверждает корректность доказательства. В эксперименте существующие fuzz-тесты переводили в спецификации для скомпилированных RISC-V-бинарников под Linux. Claude писал доказательства на Rocq, а ядро Rocq проверяло их независимо от модели.
- 239 тестовых точек входа получили доказательства отсутствия сбоев в заданных условиях
- 123 библиотеки с открытым исходным кодом вошли в исследование
- около 180 млн строк Rocq составил общий объём доказательств
- до 64 МБ — максимальный размер входных данных, охваченный основной спецификацией
Источник: Anthropic, 22 октября 2026 года.
По данным Anthropic, работа велась несколько недель. Если в процессе доказательства находилась ошибка, Claude мог предложить исправление, после чего спецификацию строили заново и проверку повторяли. Среди обнаруженных случаев были обращения за границы памяти и логические дефекты, которые обычному фаззингу было трудно воспроизвести.
Авторы также проверяли другие сценарии. В одном из них модель подготовила формальную спецификацию формата zlib и доказала соответствие ей реализации в ядре Linux на уровне x86-бинарника. В другом Claude создал интерпретатор части Python на Rust и формально сопоставил его с описанием поведения CPython; при дополнительном прогоне 1,7 млн случайно сгенерированных программ результаты совпали в 99,95% случаев.
Ограничения здесь существенны. Основная серия доказательств относится к однопоточным статическим RISC-V-бинарникам, работающим в описанной модели Linux и с фиксированным бюджетом памяти. Проверялась не вся библиотека, а доступный из конкретной тестовой точки код. Кроме того, доказательство гарантирует только свойства, записанные в спецификации: оно не исключает ошибки, которые эта спецификация или модель среды не охватывает.
Публичная часть результатов доступна в репозитории Theorem. Там отдельно указано, что опубликованные доказательства относятся к конкретным бинарным сборкам и проверяемым свойствам, а не подтверждают полную безошибочность библиотек. Это делает работу воспроизводимой и одновременно задаёт границы выводов.
Практическое значение подхода — в возможности переносить формальную верификацию из узких критически важных проектов в обычную разработку. Пока метод требует больших вычислительных затрат и тщательно подготовленных моделей среды, но повторно используемые доказательства могут снижать стоимость последующих проверок.
Пока никто не ответил. Начните обсуждение.