Anthropic заявляет, что Claude написал формальные доказательства того, что 123 библиотеки с открытым исходным кодом не могут аварийно завершиться

В рамках сотрудничества с Theorem Anthropic заявляет, что использовала Claude для доказательства свойств безопасности на уровне ассемблера (RISC-V) более чем в 100 реальных библиотеках с открытым исходным кодом. Компания называет это первым крупномасштабным применением ИИ для формальной верификации промышленного ПО на таком уровне.

По данным Anthropic:

• Что доказали: для 239 точек входа в фаззинг-тесты в 123 библиотеках OSS-Fuzz программы всегда завершаются штатно — без ошибок безопасности памяти и сбоев проверок — при любых входных данных размером до 64 МБ. Это верно при следующих допущениях: однопоточный статический бинарный файл с фиксированным объёмом памяти на процессоре RISC-V под управлением Linux. Доказательства составляют около 180 миллионов строк кода на Rocq, проверенных системой проверки доказательств Rocq.
• Как: существующий фаззинг-тест каждой библиотеки преобразовали в спецификацию («этот тест никогда не аварийно завершается»), а Claude написал доказательство, по пути исправляя найденные ошибки. Anthropic сообщает, что так удалось обнаружить сотни ошибок, в том числе такие, до которых фаззер вряд ли добрался бы, например запись за пределами буфера, для которой нужны редкие входные данные размером 20 МБ, а также повторно обнаружить CVE-2026-56132 в libexpat.
• Другие эксперименты: Claude доказал, что реализация zlib в ядре Linux соответствует спецификации RFC 1950 на уровне бинарного кода x86, а также создал интерпретатор Python на Rust, поведение которого совпало с CPython в 99,95% из 1,7 миллиона случайных программ. Anthropic также сообщает, что попытки формальной верификации широко используемой программы для чтения PDF выявили за одну неделю столько же уязвимостей, сколько обычно сообщают за год.
• Стоимость: доказательства могут требовать сотни миллионов токенов. На 36 небольших задачах верификации, по данным Anthropic, Opus 5.5 доказывает половину из них, расходуя примерно на 40% меньше токенов, чем Opus 5; кроме того, агентам, совместно использовавшим доказательства, потребовалось на 17% меньше токенов.

Anthropic публикует часть доказательств, а также семантику RISC-V и Linux. Theorem предлагает запускать тот же процесс для других проектов с открытым исходным кодом и публикует навык Claude для проверки собственного кода. Anthropic отмечает, что это не доказывает отсутствие ошибок в библиотеках: оставшиеся ошибки могли бы находиться в доверенных компонентах или за пределами области охвата доказательств.