Клод написал 180 миллионов строк математического доказательства в ходе первой крупномасштабной формальной проверки ИИ программного обеспечения с открытым исходным кодом

Полный отчет

22 октября компания Anthropic объявила на своей официальной исследовательской странице: в сотрудничестве с компанией по проверке программного обеспечения «Теорема» Клод официально проверил свойства безопасности на уровне сборки RISC-V в 123 реальных библиотеках с открытым исходным кодом, взятых из Google OSS-Fuzz, охватывающих 239 точек входа в программу. Компания называет это «первой крупномасштабной попыткой использовать ИИ для формальной проверки производственного программного обеспечения на уровне ассемблерного кода».

Масштаб поразителен: около 180 миллионов строк доказательств Рока, при этом типичное доказательство составляет около 600 000 строк, охватывающих двоичные файлы со средней длиной 18 000 инструкций RISC-V — все это завершено за считанные недели. Ядро Rocq независимо проверяет каждое доказательство, поэтому построчная проверка вручную не требуется.

Этот метод преобразует существующие нечеткие тесты в математические спецификации: для любого ввода размером менее 64 МБ однопоточный статически связанный двоичный файл RISC-V в Linux всегда должен завершаться нормально, без нарушений безопасности памяти. Когда Claude заподозрил ошибку в середине проверки, он напрямую исправил код и повторно проверил новую спецификацию.

По пути всплыли сотни ошибок, в том числе опустошение счетчика в декомпрессорной копии, приводящее к записи за пределами допустимого диапазона (запускаемое только вводами ~20 МБ с одним редким макетом), чтение за пределами допустимого диапазона в декодере изображений и повторное обнаружение CVE-2026-56132 в libexpat — некоторые уязвимости скрывались годами.

Anthropic сам признает наличие ограничений: пройденная формальная проверка не означает отсутствие ошибок — доказательства охватывают только однопоточные статические двоичные файлы RISC-V, тогда как большая часть кода фактически работает на x86/ARM. Компания опубликовала часть доказательств на GitHub для независимой проверки, и в компании Theoreom говорят, что она будет использовать тот же конвейер для других проектов с открытым исходным кодом.

Побочные результаты также заслуживают внимания: было доказано, что реализация zlib в ядре Linux соответствует RFC 1950 на двоичном уровне x86, а большое подмножество интерпретатора Python, написанного на Rust, соответствует поведению CPython на 99,95% из более чем 1,7 миллиона рандомизированных программ.