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

Подробно

Что именно сделал Claude и почему не «верифицировал 123 библиотеки»?

Anthropic заявляет доказательства для 239 отдельных fuzz-entry points в 123 библиотеках OSS-Fuzz. Это не доказательство корректности всего кода каждой библиотеки, поэтому формулировка «верифицировал 123 библиотеки» неточна. Исследование выполнила Frontier Red Team Anthropic совместно с Theorem, работа заняла несколько недель.

Объект доказательства - конкретные скомпилированные RISC-V-бинарники fuzz-тестов, а не исходный код. Бинарник, формальная семантика RISC-V/Linux и требуемое свойство механически задают спецификацию. Claude пишет доказательство, а ядро Rocq проверяет, что оно соответствует спецификации.

«Formally verified» не означает «без ошибок».

Так авторы исследования сами оговаривают границы результата.

Какую гарантию дают эти доказательства?

Для охваченной точки входа ни один допустимый вход меньше 64 MB, ни один моделируемый ответ Linux и ни одна моделируемая раскладка памяти не приводят к оговорённому классу сбоев. Гарантия действует при заданных предположениях: однопоточный статически скомпонованный бинарник, фиксированный бюджет памяти, процессор RISC-V и Linux. Типичные реальные x86/ARM-сборки с динамической glibc она напрямую не охватывает.

В приложении «сбой» определён как fault, abort или поведение, которого нет в формальной модели. Обычная и ASan-сборки сравниваются по прочитанным и записанным байтам, коду или сигналу завершения и финальному состоянию файловой системы, но не по производительности. В основном тексте предел входа назван «64 MB», в приложении - «64 MiB»; источники это расхождение не объясняют.

Модель Linux Process Semantics охватывает 64-битные RISC-V-процессы на Linux. Её авторы прямо называют модель неполной и содержащей непроверяемые предположения: доказательство применимо к реальности настолько, насколько корректна модель.

Какого масштаба доказательства и какие ошибки нашли?

Успешные доказательства составляют около 180 миллионов строк Rocq. Типичное доказательство - около 600 000 строк для бинарника медианной длиной 18 000 инструкций RISC-V. Всего Claude сгенерировал около 1 миллиарда строк, но проверяющее ядро приняло лишь около 180 миллионов. Проверка одного типичного доказательства занимает от 30 минут до нескольких часов процессорного времени.

По заявлению Anthropic, попытки доказательства выявили сотни ошибок. Среди примеров:

• underflow счётчика с записью за границы буфера при редком входе около 20 MB;
• чтение за границами в декодере изображения при входе 64 MB и потреблении более 2 GB памяти;
• ошибка при особой последовательности операций с двумя дескрипторами одного файла;
• логическая ошибка, из-за которой ограничение загрузки файлов применялось не всегда.

Полного перечня, разбивки по библиотекам, серьёзности и статусу исправления нет. Неясно и то, сколько ошибок найдено именно доказательством, а сколько сопутствующим анализом. Доказательства, способные выдать ещё не исправленные уязвимости, Anthropic не публикует.

Что известно о CVE-2026-56132 в libexpat?

Это единственная конкретная находка, подтверждённая независимо. Anthropic называет её повторным обнаружением (rediscovery), а не новой уязвимостью. Red Hat описывает ошибку как heap-based buffer overflow в libexpat с оценкой 6,9 балла по CVSS 3.1 и возможными последствиями вплоть до выполнения кода, чтения и изменения памяти и отказа в обслуживании.

Исправление приняли в upstream libexpat 20 июня 2026 года. В pull request указано «Reported-by: Trail of Bits, in collaboration with Anthropic». По публичному реестру Anthropic, уязвимость обнаружила Claude Mythos Preview, а Trail of Bits провела triage и раскрытие и признала находку истинным срабатыванием. Это подтверждает одну находку, но не проверяет результат по всем 123 библиотекам.

Что можно проверить самостоятельно?

Открытый репозиторий Theorem содержит доказательства для 60 точек входа в 25 библиотеках, включая OpenSSL, simdjson, zstd, bzip2, libpcap, mbedTLS и cJSON. Используется Rocq 9.2.0. Доказательства относятся к статическим riscv64-бинарникам, собранным clang 20.1.8 с musl. Для ASan-доказательств оговорён бюджет обычной сборки 2 GiB, для UBSan - 16 GiB.

Репозиторий включает закреплённые версии бинарников и инструментов, контрольные суммы SHA-256, Docker-образ проверяющей среды и CI. Проверка одного доказательства на 16 ядрах может потребовать до 20 GiB оперативной памяти. Полную заявленную совокупность из 239 точек входа внешние стороны воспроизвести пока не могут. Редакция проверку не запускала.

О чём предупреждают сами авторы публичного релиза?

В README сказано, что доказательство не утверждает корректность всей библиотеки и не охватывает код, недостижимый из точки входа. Оно также не исключает ошибки, которых не видят санитайзеры, и не относится к x86-64-сборкам OSS-Fuzz.

Отдельно указано, что ни одно опубликованное доказательство не является halts statement и потому не исключает бесконечное выполнение. В основном материале Anthropic при этом говорится о программах, которые «always exit normally». Источники не поясняют, идёт ли речь о разных наборах или типах утверждений.

Как это оценивают независимые эксперты?

Автор explainx.ai Yash Thakker пишет, что главный вывод - не «ИИ доказал корректность ПО». Важнее возможность поручать агентам трудоёмкое написание доказательств, а окончательную проверку оставлять формальному ядру. Он подчёркивает, что результат зависит от спецификации, модели машины и доверенной базы.

В приложении Anthropic приведена оценка неназванного эксперта по формальной верификации: доказательства агентов так же корректны, как другие доказательства той же теоремы, но неизвестно, масштабируется ли их многословный стиль. Независимость этого эксперта не установлена.

Материал не найден ни как препринт на arXiv, ни как рецензируемая статья или доклад конференции. Это корпоративная публикация с техническим приложением, независимой полной репликации пока нет. Заявление о «первой крупномасштабной» ИИ-верификации промышленного ПО на уровне ассемблера сделано с оговоркой «to our knowledge» и независимо не доказано.

Что показали сравнения моделей и дополнительные эксперименты?

По данным Anthropic, на 36 уменьшенных задачах из реального OSS-Fuzz модель Opus 5.5 доказывала половину задач примерно на 40% меньшим числом токенов, чем Opus 5. Каждой задаче дали три независимые одиночные попытки с бюджетом 5 миллионов токенов. Когда агенты работали в общем рабочем пространстве, они тратили на 17% меньше токенов, чем при изолированной работе. Это внутренние эксперименты разработчика, а не независимые бенчмарки. Какие версии Claude выполняли основной прогон по 123 библиотекам, не указано.

В отдельном кейсе, не входящем в показатель 123 библиотек, Claude написал на Rust интерпретатор подмножества Python и доказал его соответствие формальной семантике через Verus. Сравнение более чем на 1,7 миллиона случайных программ показало 99,95% совпадений с CPython.

Кто и на каких условиях может воспользоваться OSS Verify?

Theorem открыла OSS Verify для established open-source проектов. Основной maintainer может подать проект с публичным репозиторием и fuzz target, услуга заявлена как бесплатная. По описанию Theorem, если в библиотеке есть ошибка, из-за которой тест аварийно завершается, система найдёт её и конфиденциально сообщит разработчикам. Это заявление заинтересованной стороны.

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

Какова предыстория работы?

Формальная верификация реального системного ПО исторически была крайне трудоёмкой. Показательный пример - комплексная машинно-проверенная верификация микроядра seL4, обзор которой вышел в ACM Transactions on Computer Systems в феврале 2014 года.

Незадолго до нового исследования, 4 сентября 2026 года, Anthropic сообщила, что Claude за 11 дней в значительной степени автономно подготовил 13 миллионов строк Lean и 29 500 промежуточных теорем для формализации Великой теоремы Ферма. Тогда речь шла о математике, а не о ПО.

29 сентября 2026 года (материал дополнен 19 октября) Theorem представила план Verified Software Stack на примере nixpkgs. Компания оценила гипотетическую проверку 95% машинного кода экосистемы к концу 2027 года примерно в 134 млн долларов. Это прогноз самой Theorem, а не завершённый проект.