Claude доказал, что 239 функций из 123 открытых библиотек не падают ни на каких данных

22 октября Frontier Red Team Anthropic вместе с компанией Theorem опубликовала исследование о том, что языковые модели делают формальную верификацию (математическое доказательство того, что программа ведёт себя строго по заданным правилам для любых входных данных) практичной в больших масштабах. По словам авторов, это первое крупное применение ИИ для формальной проверки промышленного ПО на уровне ассемблерного кода.

Что произошло

Классическая верификация очень дорога: ядро seL4 написали примерно за 2 человеко-года, а доказывали его корректность около 20. При этом в ядре Linux недавно раскрыли более 1000 уязвимостей. Авторы считают, что обычной защиты уже недостаточно и нужен способ доказывать отсутствие багов.

• Материал — 123 открытые библиотеки из Google OSS-Fuzz (программы непрерывного фаззинга, то есть проверки кода случайными входными данными).
• Существующие фазз-тесты скомпилировали в бинарники RISC-V, семантика RISC-V и Linux от Theorem превратила их в формальные спецификации, Claude писал доказательства, а программа Rocq их проверяла.
• Доказано, что для 239 точек входа программа не падает из-за ошибок памяти или проваленных проверок на любых входах до 64 МБ.
• Всего около 180 млн строк доказательств; типичное — около 600 000 строк для бинарника с медианой 18 000 инструкций.
• Работа заняла несколько недель.

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

Пытаясь доказать корректность, Claude нашёл и исправил сотни ошибок. Среди примеров — запись за границы буфера в декомпрессоре, срабатывающая лишь на входах около 20 МБ с редкой раскладкой; чтение за границы в декодере изображений, требующее входа в 64 МБ и более 2 ГБ памяти; повторное обнаружение CVE-2026-56132 в libexpat. Нашлась и логическая ошибка без падения: функция ограничения доступа к файлам срабатывала не всегда. Помимо OSS-Fuzz, Claude формально описал стандарт zlib (RFC 1950) и доказал соответствие ему реализации из ядра Linux на уровне x86. Ещё один эксперимент — интерпретатор подмножества Python на Rust с доказательством соответствия семантике CPython: на 1,7 млн случайных программ поведение совпало в 99,95% случаев. Попытки верифицировать PDF-ридер за неделю дали столько же уязвимостей, сколько обычно сообщают за год.

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

Для разработчиков и компаний это меняет экономику безопасности. Фаззинг ищет баги, но не гарантирует их отсутствия; доказательство гарантирует в рамках спецификации. Если модель берёт на себя написание доказательств, проверка критичных библиотек становится вопросом вычислений, а не многолетней работы специалистов. Модели заметно дешевеют в этой работе: на 36 небольших задачах из OSS-Fuzz Opus 5.5 доказал половину, потратив примерно на 40% меньше токенов, чем Opus 5. Агенты с общим хранилищем доказательств расходовали на 17% меньше токенов, чем работающие поодиночке. При этом отдельное доказательство может стоить сотни миллионов токенов.

Авторы честно перечисляют ограничения. Проверка не подтверждает, что сама спецификация соответствует реальности. Доказательства сделаны для статических бинарников с musl на RISC-V, а большинство пользователей запускают динамические сборки с glibc на x86 или ARM. Проверены не все точки входа, а AddressSanitizer ловит не все ошибки памяти. Чтобы не допустить читерства, команда штрафовала патчи, менявшие поведение кода, и проверяла их вручную.

Что дальше

Anthropic публикует часть доказательств, семантики RISC-V и ОС, а также навык Claude для разработчиков. Theorem предлагает прогонять этот конвейер для других проектов, а в её дорожной карте — экосистема Nix, включая glibc, OpenSSL и cURL. Ставка в том, что после доказательства общих библиотек проверка остального ПО резко упростится, а формальная верификация станет такой же привычной, как фаззинг сегодня.