Claude доказал безопасность 123 библиотек на уровне RISC-V-кода

Anthropic и компания Theorem опубликовали результаты проекта, в котором Claude в автономном режиме писал формальные доказательства корректности для реального open-source кода. Модель доказала отсутствие падений для 239 точек входа в 123 библиотеках из Google OSS-Fuzz. Доказательства работают не с исходниками, а со скомпилированными инструкциями RISC-V и в сумме занимают около 180 млн строк на Rocq. Раньше такая работа требовала лет усилий узких специалистов, поэтому её применяли только там, где ошибка стоит слишком дорого, например в авионике Airbus.

Фаззинг-тест как готовая спецификация

Главная проблема формальной верификации в том, что сначала нужно объяснить, что значит «корректно». Для декодера PNG есть RFC 2083, а для текстового редактора или браузера внятной спецификации нет. Исследователи обошли это так: взяли существующие фаззинг-тесты разработчиков и превратили условие «тест никогда не падает» в формальную спецификацию. Её описали поверх модели того, как любой бинарник под RISC-V исполняется в Linux.

Фаззер перебирает огромное число полуслучайных входов, но полного покрытия не гарантирует. Доказательство даёт именно гарантию: если Claude доказал, что тест не упадёт ни на каком входе меньше 64 МБ, то фаззинг этой точки входа на RISC-V больше ничего не найдёт. OSS-Fuzz собирает C и C++ программы с AddressSanitizer, так что любое неправильное обращение к памяти считается падением. Поэтому в доказанное свойство автоматически входит memory safety, главный источник уязвимостей.

Что именно получилось

Проект занял несколько недель. Критерий успеха: Claude пишет доказательство, а проверяет его ядро Rocq, и человеку не нужно читать сотни тысяч строк. Доверять приходится трём вещам: формальным моделям RISC-V и Linux-процессов, точным формулировкам теорем и самому Rocq.

• 123 библиотеки OSS-Fuzz, 239 точек входа
• около 180 млн строк Rocq, типичное доказательство около 600 тысяч строк
• медианный бинарник: 18 000 инструкций RISC-V
• гарантия: корректный выход без ошибок памяти и сбоев assertions на любом входе до 64 МБ
• допущения: однопоточный статический бинарник, фиксированный бюджет памяти, RISC-V и Linux

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

Баги, которые фаззер не нашёл бы

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

• underflow счётчика в копии декомпрессора, ведущий к записи за границы буфера, только на входах около 20 МБ с редкой структурой
• чтение за границами в декодере изображений, которому нужен вход 64 МБ и больше 2 ГБ памяти
• чтение за границами в другой библиотеке после определённой последовательности вызовов через два дескриптора одного файла
• повторное обнаружение CVE-2026-56132 в libexpat, требующее глубокой вложенности
• логическая ошибка без падений: функция ограничения загружаемых файлов работала не всегда

Побочный эффект тоже важен: даже неудачная попытка доказательства вскрывает реальные дефекты. Кроме того, фаззинг-тесты часто проверяют высокоуровневые свойства, например кодирование-декодирование без потерь. Для алгоритма сжатия LZO тест утверждает, что распаковка сжатых данных возвращает оригинал. Если свойство нарушено, программа падает, и доказательство отсутствия падений равносильно доказательству самого свойства. Для cpp-httplib Claude пришлось отдельно исключить переполнение стека из-за глубокой рекурсии в деструкторе std::set.

Практический вывод для команд

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

Anthropic публикует часть доказательств, модели RISC-V и ОС, а также спецификации для тестов, которые доказать не удалось. Theorem предлагает прогнать тот же пайплайн на других open-source проектах и выпускает Claude skill для самостоятельной верификации. Разработчикам, которые когда-то пробовали формальные методы на более слабых моделях и отказались, стоит вернуться к вопросу. Начать разумно с проекта, у которого уже есть качественные фаззинг-тесты: спецификация там почти готова. Параллельно авторы пробуют те же методы на zlib и на проверке поведенческой эквивалентности интерпретатора Python, написанного на Rust.