Claude доказал безопасность 123 открытых библиотек: 180 млн строк доказательств

22 октября Frontier Red Team компании Anthropic и фирма Theorem опубликовали результаты проекта, в котором Claude за несколько недель написал формальные доказательства безопасности для 123 открытых библиотек. Доказательства построены не для исходного кода, а для скомпилированных бинарников RISC-V: модель доказывала, что программа всегда завершится нормально и не вызовет ошибку памяти ни на каком входе меньше 64 МБ.

«Claude исправил найденные ошибки и затем доказал, что падений нет ни на каком входе до 64 МБ — для 239 точек входа в 123 разных библиотеках OSS-Fuzz». — Anthropic

Как тесты превратили в доказательства

За основу взяли фаззинг-тесты из инициативы Google OSS-Fuzz. Спецификацию сгенерировали автоматически из самого теста: «этот вход не падает ни на каком входе меньше 64 МБ». Claude писал доказательство на языке Rocq (бывший Coq), а ядро Rocq механически проверяло, что оно действительно доказывает заявленное свойство, — вручную просматривать почти ничего не нужно.

• Итог: 239 точек входа в 123 библиотеках.
• Объём: около 180 млн строк Rocq; типичное доказательство — примерно 600 тысяч строк для бинарника медианной длиной 18 тысяч инструкций RISC-V.
• Разница с тестами: фаззинг такой гарантии не даёт в принципе — он перебирает входы и не может покрыть все пути.

Какие ошибки нашлись

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

Что оговаривают авторы

Доказательства верны при допущениях: однопоточный статический бинарник с фиксированным бюджетом памяти на процессоре RISC-V под управлением Linux. Доверять нужно три вещи — формальным моделям RISC-V и процессов Linux, точным формулировкам доказанных теорем и ядру проверки Rocq. Это не доказательство отсутствия всех ошибок: вне области остаются дефекты в самих доверенных компонентах. Anthropic публикует подмножество доказательств и семантику на GitHub, а Theorem предлагает прогнать тот же конвейер для других проектов и выложила навык для Claude, чтобы команды могли начать сами.

Почему это важно

Для сравнения: ядро seL4 написали за два человеко-года, а формально верифицировали двадцать. Если стоимость доказательства падает до нескольких недель на сотню библиотек, гарантии перестают быть привилегией авионики и оборонных систем и могут стать частью обычного CI — тем более что ИИ уже научился находить и связывать уязвимости в чужом коде.

Источники: Anthropic, Theorem Labs (GitHub), unite.AI.