Anthropic: Claude доказал отсутствие сбоев в 239 точках входа 123 библиотек

Anthropic в сотрудничестве с компанией Theorem сообщила, что Claude написал формальные доказательства безопасности на уровне ассемблера (RISC-V) для более чем 100 реальных библиотек с открытым кодом. В теле статьи точнее: 239 точек входа в 123 библиотеках из проекта Google OSS-Fuzz. Авторы утверждают, что, по их сведениям, это первая крупная попытка применить ИИ к формальной верификации промышленного ПО на уровне ассемблерного кода.

Отправная мысль статьи: в большинстве программ полно ошибок, которые ИИ теперь легко находит и использует, а привычных средств защиты уже недостаточно. Авторы приводят пример ядра Linux: в нём недавно раскрыли более 1000 уязвимостей. Формальная верификация (математическое доказательство того, что код всегда соблюдает заданные правила) могла бы дать гарантию, но раньше требовала многолетней работы экспертов. Пример из статьи: ядро seL4 реализовали за два человеко-года, а формально верифицировали за 20. Поэтому метод применяли только в критически важных системах, например в авионике Airbus.

Главная проблема масштабирования: нужно сначала определить, что значит «корректно» (спецификацию). Авторы решили её так: взяли уже имеющиеся фазз-тесты разработчиков (тесты, где движок подаёт на вход программе огромное число полуслучайных и мутированных данных в поисках падения) и превратили их в спецификацию над скомпилированными инструкциями RISC-V. Спецификация гласит: тест не упадёт ни на каком входе меньше 64 МБ. Если Claude это доказывает, фаззинг этой точки входа на RISC-V становится излишним: он уже ничего не найдёт.

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

Ручной проверки почти не требуется: корректность доказательств проверяет программа-проверяющий Rocq. Доверять приходится только трём вещам: формальным моделям RISC-V и процессов Linux, точным формулировкам доказанных теорем и самому Rocq. Авторы подчёркивают, что это не значит «в библиотеках нет ошибок»: оставшиеся ошибки могут быть в этих доверенных компонентах или вне области доказательства. Укреплять их, по словам авторов, куда проще, чем отлаживать каждую строку кода, а число защищённых проектов можно наращивать без роста доверенной части.

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

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

Ключевые факты

• Claude за несколько недель доказал отсутствие падений на любых входах до 64 МБ для 239 точек входа в 123 библиотеках OSS-Fuzz; доказательства работают на уровне скомпилированного кода RISC-V.
• Объём доказательств на Rocq: около 180 миллионов строк суммарно, типичное доказательство около 600 000 строк, бинарные файлы медианной длиной 18 000 инструкций; корректность проверяет Rocq, доверять нужно моделям RISC-V и Linux, формулировкам теорем и самому Rocq.
• Спецификацией послужили готовые фазз-тесты: «тест не падает ни на каком входе до 64 МБ»; доказательство делает фаззинг этой точки входа на RISC-V излишним.
• В ходе работы обнаружены сотни ошибок, Claude сам их исправлял; среди находок ошибка, проявляющаяся на входе около 20 МБ, и повторное открытие CVE-2026-56132 в libexpat.
• Результат действует при допущениях (однопоточный статический бинарный файл, фиксированная память, RISC-V, Linux) и, по словам авторов, не означает, что в библиотеках нет ошибок.

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

Формальная верификация годами считалась слишком дорогой для обычных проектов: пример из статьи, 2 человеко-года на реализацию ядра seL4 против 20 на его верификацию. Anthropic показывает масштаб, который раньше был недостижим: 239 точек входа в 123 библиотеках за несколько недель работы Claude. Это сдвигает вопрос от «можно ли вообще» к «сколько это стоит». Авторы связывают это с ростом числа находимых ИИ уязвимостей: в ядре Linux недавно раскрыли более 1000 уязвимостей, и привычной защиты, по их мнению, уже недостаточно. Утверждение о первенстве оговорено словами «по нашим сведениям».

Кому это важно

Мейнтейнерам библиотек на C и C++, у которых уже есть фазз-тесты в OSS-Fuzz: именно такие тесты Anthropic превращает в спецификации. Командам, отвечающим за безопасность критичной инфраструктуры, и специалистам по формальным методам, которые смогут проверять опубликованные доказательства и модели. Также тем, кто выбирает, какие гарантии безопасности можно получить от ИИ-разработки, а не только от ИИ-поиска ошибок.

Как это применить

Theorem предлагает запустить тот же конвейер для других открытых проектов и публикует навык (skill) для Claude, чтобы разработчики могли начать верифицировать собственный код. Anthropic публикует часть доказательств, формальные модели RISC-V и ОС и спецификации для фазз-тестов, которые не удалось доказать; их можно проверить и использовать повторно. Авторы советуют попробовать формальную верификацию с LLM даже тем, у кого она не сработала на менее способных моделях. Стоимость запусков и цены в тексте не названы.

Можно ли доверять

Источник, собственная публикация Anthropic, выполненная вместе с Theorem; независимой оценки в этом материале нет. Сами авторы приглашают к независимой проверке и публикуют часть доказательств и доверенные компоненты. Сильная сторона метода: результат проверяет программа Rocq, а не человек, поэтому читать сотни миллионов строк доказательств не нужно. Слабое место, на которое указывают сами авторы: надёжность держится на моделях RISC-V и Linux, формулировках теорем и самом Rocq. Точное число найденных ошибок названо только как «сотни», сколько точек входа остались недоказанными, в разобранной части не сообщается.

Риски и подводные камни

Доказано лишь отсутствие падений (ошибок памяти и сработавших проверок) при допущениях: однопоточный статический бинарный файл, фиксированный бюджет памяти, процессор RISC-V, ОС Linux, вход меньше 64 МБ. Авторы прямо пишут, что до исправления всех возможных ошибок ещё далеко, а оставшиеся ошибки могут находиться в доверенных компонентах или вне области доказательства. Логические ошибки, не приводящие к падению, такой спецификацией сами по себе не ловятся: Claude нашёл одну лишь попутно. Для других архитектур и ОС нужно стандартизировать семантику; это названо «вполне достижимым», но не сделанным.

«Передовые модели теперь могут полностью автономно создавать доказательства корректности для реального программного обеспечения.»

— Авторы статьи, Anthropic