Anthropic заявляет, что Claude доказал свойства безопасности для 123 библиотек

Anthropic опубликовала исследование 22 октября 2026 года, сообщив, что Claude создал проверенные машиной формальные доказательства свойств безопасности на уровне ассемблерного кода RISC-V для 239 точек входа fuzz-тестов в 123 библиотеках с открытым исходным кодом в сотрудничестве с Theorem.

По данным Anthropic, Claude исправил найденные ошибки, а затем доказал, что при любом входе размером менее 64 МБ и любом смоделированном ответе операционной системы Linux и расположении памяти программы всегда завершаются штатно, не вызывая ошибок безопасности памяти и не нарушая проверки утверждений. Доказательства предполагают, что программа выполняется как однопоточный статический исполняемый файл с фиксированным объемом памяти на процессоре RISC-V под управлением Linux. Anthropic сообщила, что доказательства состоят примерно из 180 миллионов строк на Rocq; типичное доказательство насчитывает около 600 000 строк и охватывает двоичные файлы с медианной длиной 18 000 инструкций RISC-V. По словам компании, насколько ей известно, это первая масштабная попытка применить ИИ для формальной верификации промышленного программного обеспечения на уровне ассемблерного кода.

Часть доказательств вместе с лежащей в их основе семантикой RISC-V и операционной системы публикуется на GitHub. Anthropic сообщила, что также публикует созданные для проекта доверенные компоненты, которые еще не были доступны широкой публике, полные доказательства для fuzz-тестов, не требовавших исправления кода, и спецификации fuzz-тестов, которые не удалось доказать. При этом компания не публикует доказательства, способные раскрыть неисправленную ошибку.

От fuzz-тестов к формальным доказательствам

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

Anthropic сообщила, что применила этот процесс к сотням проектов в инициативе Google OSS-Fuzz, которая обеспечивает непрерывное fuzz-тестирование соответствующих требованиям проектов с открытым исходным кодом и автоматически инструментирует программы на C и C++ с помощью AddressSanitizer — инструмента, который аварийно завершает программу при любом некорректном обращении к памяти. В приложении от 22 октября 2026 года полностью сформулирована доказанная теорема: для всех входных данных размером менее 64 МиБ и всех вариантов расположения памяти ни двоичный файл, инструментированный с помощью ASan, ни обычный двоичный файл не выдают ошибку, не прерывают работу аварийно и не демонстрируют неучтенное поведение; при этом оба файла формируют идентичные последовательности операций чтения и записи, одинаково завершают работу и оставляют файловую систему в одинаковом конечном состоянии.

В приложении говорится, что за время работы Claude написал около миллиарда строк на Rocq, из которых примерно 180 миллионов прошли проверку доказательств. Для точки входа 391-строчного парсера cJSON было создано доказательство объемом 630 000 строк, а для fftw3, в которую при компоновке было включено 51 000 строк кода, — доказательство объемом 480 000 строк. Поскольку Claude разрешалось исправлять код до завершения доказательства, Anthropic сообщила, что штрафовала за исправления, начисляла дополнительное вознаграждение за доказательство того, какие входные данные изменились из-за исправления, а также регистрировала и проверяла все исправления, чтобы препятствовать манипулированию системой вознаграждений.

Ошибки, обнаруженные при попытках доказательства

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

Claude также обнаружил логические ошибки, которые не приводят к сбою, в том числе проблему с ограничением на файлы, загружаемые приложением: это ограничение соблюдается не всегда. Anthropic сообщила, что попытки верифицировать несколько широко используемых критически важных приложений выявили ранее неизвестную логическую ошибку, которая оставалась незамеченной более десяти лет. Кроме того, при попытке верифицировать широко используемую программу для чтения PDF-файлов за одну неделю компания обнаружила столько же ошибок безопасности, сколько обычно сообщается за год.

Дополнительные эксперименты и выводы об эффективности

Помимо OSS-Fuzz, Anthropic поручила Claude составить формальную спецификацию RFC 1950 — технического документа, описывающего формат сжатия zlib, — а затем доказать, что реализация zlib в ядре Linux корректно ей соответствует. Claude непосредственно доказал корректность двоичного файла, скомпилированного для x86, используя созданную им формальную семантику набора инструкций x86. Anthropic сообщила, что повторила этот процесс еще для полудюжины широко используемых библиотек и обнаружила небольшие неисправимые в рамках эксплуатации ошибки в крайних случаях, о которых сообщают сопровождающим проектов. Компания также сообщила, что при создании семантики x86 были выявлены сотни ошибок в официальной справочной документации и меньшее число ошибок в самом оборудовании. Кроме того, пошаговое выполнение семантики позволяет загрузить пользовательское окружение Ubuntu на ядре Linux.

В другом эксперименте Claude создал на Rust интерпретатор для значительной части Python и с помощью инструмента верификации Verus доказал, что тот соответствует семантике CPython, изложенной в научной статье. В техническом приложении говорится, что были доказаны все 17 уровней интерпретатора, причём теорема утверждает: «Всякий раз, когда интерпретатор возвращает результат, этот результат соответствует предписанию формальной семантики». Anthropic сообщила, что эмпирические испытания на 1,7 миллиона случайно сгенерированных программ на Python показали поведение, идентичное CPython, в 99,95% тестов; из семи намеренно внесённых ошибок пять не выявило случайное тестирование, тогда как все семь нарушали доказательство.

Чтобы измерить эффективность, Anthropic создала 36 небольших задач на верификацию, сократив реальные точки входа OSS-Fuzz. Получившиеся программы содержали от 283 до 2 491 инструкции, размер входных данных был ограничен 64 байтами, а AddressSanitizer заменили средой выполнения «mini-ASan» объёмом около 100 инструкций. По сообщению Anthropic, Opus 5.5 решает половину задач, используя примерно на 40% меньше токенов, чем Opus 5. Anthropic также сообщает, что агентам, которым разрешили копировать доказательства друг друга в общем рабочем пространстве, требовалось на 17% меньше токенов, чем агентам, работавшим поодиночке; некоторые агенты справились после того, как прежде не смогли решить задачу самостоятельно, а работавшие в одиночку агенты не смогли завершить два доказательства. Компания заявила, что тот же эффект повторного использования проявился в масштабах работы над OSS-Fuzz: команды агентов копировали готовые доказательства и адаптировали их, поскольку значительная часть каждого доказательства относится к общему коду инициализации среды выполнения C и AddressSanitizer.

Заявленные ограничения и программа OSS Verify

Anthropic подчёркивает, что доказательства не означают, будто в библиотеках нет ошибок: оставшиеся ошибки могут находиться в доверенных компонентах или за пределами области действия доказательств. Доказательства охватывают однопоточные статические бинарные файлы для RISC-V, связанные с musl libc, тогда как большинство пользователей запускают эти библиотеки на x86 или ARM и динамически связывают их с glibc; кроме того, AddressSanitizer обнаруживает не все ошибки, связанные с безопасностью памяти. Компания заявила, что рассчитывает: по мере совершенствования моделей эти ограничения станет возможно преодолеть.

Theorem бесплатно предлагает такой же конвейер подходящим проектам с открытым исходным кодом в рамках программы OSS Verify. Для участия нужно отправить запрос на включение изменений, добавляющий файлы project.yaml, Dockerfile и build.sh в репозиторий программы. Theorem сообщает, что оценивает проекты примерно так же, как OSS-Fuzz, отдавая приоритет критически важной инфраструктуре, которой широко пользуются. По словам Theorem, сопровождающие проектов получают доказательство на Rocq, проверенное ядром Rocq и подтверждающее, что каждая цель фаззинг-тестирования не завершится аварийно при любых входных данных размером до 64 MiB; об обнаруженных в ходе доказательства ошибках сопровождающих конфиденциально уведомляют по электронной почте, без установленного срока раскрытия, а подготовка доказательств может занять несколько дней. В дорожной карте Theorem поставлена цель верифицировать всю экосистему Nix, включая критически важную инфраструктуру, такую как glibc, OpenSSL и cURL.