В ядре Linux, одном из самых протестированных кусков кода на планете, за последнее время раскрыли больше тысячи уязвимостей. Фаззеры гоняют миллиарды входов, тесты покрывают почти всё, а баги всё равно находятся. Anthropic 22 октября показала альтернативу: Claude доказал, что 239 точек входа в 123 open-source библиотеках не упадут ни на одном входе размером до 64 МБ. Не протестировал на большом числе примеров, а доказал для всех сразу.

Формальная верификация это метод, при котором код переводят в математическую модель и доказывают, что она всегда соблюдает заданные правила безопасности. Если доказать не получается, значит в коде есть баг, нарушающий правило, и сама причина провала подсказывает, где он. Раньше это была роскошь для авионики.

Почему верификация была роскошью

Цифры из отчёта объясняют проблему лучше любых рассуждений. Ядро seL4 написали за два человеко-года, а формально верифицировали за двадцать. Доказательства часто в разы длиннее исходного кода, а писать их умеют единицы: это отдельная специализация с собственным языком, тактиками и культурой. Поэтому верификация дожила до 2026 года в основном в Airbus и в проектах, где цена ошибки измеряется жизнями.

Anthropic зашла с другой стороны. Вместо того чтобы верифицировать всё вручную, компания дала модели задачу, которую LLM делают хорошо: перемалывать миллионы строк кода ради одной чётко определённой цели. В коллаборации с Theorem (стартап, который строит формальные семантики для реальных платформ) Claude прошёл по библиотекам Google OSS-Fuzz и написал доказательства отсутствия падений.

Что именно доказано

Формулировка важна, потому что от неё зависит вся интерпретация. Claude доказал, что скомпилированные в RISC-V программы всегда завершаются нормально: без ошибок памяти и без провалов ассертов. Условия такие: любой вход меньше 64 МБ, любое поведение смоделированной Linux-среды и любой смоделированный расклад памяти. Дополнительные допущения: однопоточный статический бинарник, фиксированный бюджет памяти, процессор RISC-V, ядро Linux.

Объём работы выглядит невероятным. 239 точек входа в 123 библиотеках, около 180 миллионов строк Rocq (это наследник Coq). Типичное доказательство занимает примерно 600 тысяч строк и покрывает бинарник медианной длиной 18 тысяч инструкций RISC-V. Проверяет всё это ядро Rocq, а не человек: вручную такой объём не читается, и это принципиальная часть замысла.

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

Как тест превращается в спецификацию

Самая сложная часть формальной верификации не доказательство, а формулировка того, что вообще значит «правильно». Для PNG-декодера всё очевидно: есть RFC 2083 и последовательность байтов. Для текстового редактора или браузера ответа нет, и это главный тормоз всей индустрии.

Anthropic обошла проблему изящно. У библиотек OSS-Fuzz уже есть фаззинг-тесты, которые падают при нарушении свойства. Значит можно взять правило «этот тест всегда проходит» и превратить его в спецификацию над скомпилированными инструкциями RISC-V. Если Claude докажет такую спецификацию, фаззинг этой точки входа больше не нужен: он не найдёт ничего нового никогда.

Механика такая: библиотека и её фаззинг-тест компилируются в RISC-V, к ним добавляются формальные семантики RISC-V и процессов Linux от Theorem, из этого механически получается спецификация, а Claude пишет доказательство. Отдельно стоит отметить, что OSS-Fuzz инструментирует C и C++ через AddressSanitizer, поэтому падения на ошибках памяти тоже попадают в модель. Именно memory safety даёт большинство уязвимостей, так что свойство не такое узкое, как звучит.

Баги, до которых фаззер не добирается

Фаззинг мутирует небольшие входы, обычно до 1 МБ, и опирается на покрытие кода. Это брутфорс без гарантий: путей бесконечно много, а входное пространство не обозримо. Отсюда класс багов, которые годами живут в коде и не всплывают, потому что для их срабатывания нужен редкий размер или редкая последовательность вызовов.

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

Были и баги, которые не падают вообще. Доказывая memory safety одной библиотеки, Claude заметил, что механизм ограничения загружаемых файлов срабатывает не всегда. Это уже логическая дыра в защите, а не порча памяти, и фаззер её принципиально не увидит, потому что краша нет.

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

Не только про память

Главный контраргумент к таким проектам звучит так: вы доказали, что программа не падает, но падение это не единственная проблема. Ответ в том, как устроены фаззинг-тесты в реальном коде. Многие из них проверяют высокоуровневые свойства: обратимость кодирования и декодирования, идемпотентность, алгебраические законы, совпадение с эталонной реализацией. Для LZO тест утверждает, что распаковка сжатого входа возвращает исходный. Тест падает при нарушении свойства, значит доказательство отсутствия падений равно доказательству самого свойства.

Иногда приходится доказывать вещи, которых автор теста не планировал. Чтобы закрыть доказательство для cpp-httplib, Claude пришлось исключить переполнение стека из-за рекурсии в деструкторе std::set. Глубина рекурсии ограничена глубиной дерева, поэтому модель доказывала уже на машинном коде, что оптимизированный алгоритм ребалансировки красно-чёрного дерева в libc++ действительно держит логарифмическую границу.

Дальше начинается самое интересное. Anthropic дала Claude спецификацию RFC 1950, документа, который определяет формат zlib, и попросила доказать, что реализация zlib в ядре Linux ей соответствует. Доказательство построили не на RISC-V, а прямо на x86-бинарнике, используя формальные семантики x86, которые Claude сгенерировал сам. Семантики получились рабочими настолько, что пошаговое исполнение на них поднимает userspace Ubuntu поверх ядра Linux. Побочный эффект: в официальной справочной документации нашлись сотни ошибок, а в самом железе несколько багов.

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

Сколько это стоит

Честная оговорка от Anthropic: доказательства могут съедать сотни миллионов токенов. Если цель сделать верификацию массовой, экономика важнее красоты.

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

Второй эффект интереснее: доказательства переиспользуются. Когда агенты работали в общем пространстве и могли копировать чужие доказательства, им требовалось на 17% меньше токенов, а часть задач решилась со второй попытки после провала в одиночку. Причина в структуре: большая доля любого доказательства приходится на инициализацию C-рантайма и AddressSanitizer, то есть на код, который есть в каждой программе. В масштабе OSS-Fuzz команды так и делали: брали готовое доказательство и адаптировали под свой бинарник.

Отсюда стратегический вывод про зависимости. Они распределены по степенному закону, поэтому верификация небольшого набора общих библиотек закрывает огромную часть софта. Theorem уже описала план покрыть экосистему Nix, включая glibc, OpenSSL и cURL. Сравнение с Mathlib напрашивается само: библиотека формальной математики в Lean выросла до почти 300 тысяч теорем от более 700 контрибьюторов именно потому, что каждое новое доказательство опирается на предыдущие.

Где доказательство не равно отсутствию багов

Самый важный абзац отчёта написан против собственного заголовка. «Формально верифицировано» не значит «без багов». Чекер проверяет, что доказательство удовлетворяет спецификации, но не может проверить, что спецификация соответствует реальности. Если баг появляется в верифицированном коде, значит модель машины разошлась с машиной.

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

Есть и риск, о котором Anthropic пишет открыто: reward hacking. Модель могла бы сделать теорему доказуемой тривиально, переписав программу в такую, которая никогда не падает. Против этого patches штрафовали, а за доказательство того, какие именно входы меняются и насколько мало их множество, давали бонус. Все патчи логировались и проверялись вручную.

Что говорят скептики

Обсуждение на Hacker News собрало 310 комментариев и главный контраргумент сформулировало точнее, чем пресс-релиз. В приложении к отчёту Anthropic сама признаёт: доказательства агентов многословны. Они раз за разом прописывают детали исполнения программы, содержимое регистров, преобразования целых, точные значения на стеке, попарную различность адресов. Стиль работает, но растёт линейно вместе со сложностью.

Из этого делают вывод о стене. Опыт других проектов агентной верификации, например MachCSL, говорит, что на сложных программах агенты упираются в комбинаторный предел многословного стиля, и дальше нужно структурировать доказательства вокруг абстракций и принципов рассуждения. Значит вопрос не в том, хватит ли токенов, а в том, научатся ли модели писать по-настоящему модульные доказательства, а не повторять один и тот же блок с точностью до адреса.

Есть и более оптимистичная рамка того же спора. В математике модели ограничены обобщением за пределы человеческого корпуса, и там действительно ждут стену. В верификации софта ограничение другое: масштаб. Программы уже написаны людьми, спецификации часто вытекают из существующих тестов, а значит задача сводится к перемалыванию объёма, которое LLM делают хорошо.

Отдельно прозвучал вопрос про модель реальности: как убедиться, что формализованная спецификация описывает именно ту программу, которую вы верифицировали, а не её удобную версию. Ответ у Anthropic структурный, а не логический: сузить список доверенных компонентов до семантик, теорем и чекера, а остальное считать проверенным. Это честнее, чем звучит, но и не закрывает вопрос целиком.

Почему это касается не только безопасников

Прагматический сдвиг здесь простой. Раньше формальная верификация была отдельным проектом на годы, который начинался с переписывания кода на языке с доказательствами. Подход Anthropic и Theorem работает на уровне скомпилированного бинарника, поэтому не требует трогать исходники и не привязывает проект к Lean, Coq или Dafny. Верификация превращается в шаг пайплайна, а не в смену технологии.

Theorem предлагает прогнать тот же пайплайн для сторонних open-source проектов и публикует Claude skill, чтобы разработчик мог начать со своей библиотеки. Подмножество доказательств и семантики уже выложены. Для команды, которая поддерживает парсер, декодер или сетевой протокол на C, это первый реальный способ получить гарантию, а не надежду.

Часто задаваемые вопросы

Можно ли считать формально верифицированный код безопасным?

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

Работает ли это на x86 и ARM?

Частично. Основной массив доказательств сделан для RISC-V, потому что для него есть готовые формальные семантики. Для x86 Anthropic показала эксперимент с zlib, где Claude сгенерировал семантики ISA самостоятельно и доказал соответствие RFC 1950 на бинарном уровне. Массовым этот путь станет, когда семантики для x86 и ARM стандартизируют так же, как для RISC-V.

Сколько стоит доказать одну библиотеку?

Дорого по токенам: суммарно речь о сотнях миллионов, а типичное доказательство занимает около 600 тысяч строк Rocq. Но цена падает с двух сторон: Opus 5.5 тратит примерно на 40% меньше токенов, чем Opus 5, а переиспользование чужих доказательств в общем пространстве экономит ещё 17%. Для небольшой библиотеки с готовым фаззинг-тестом счёт идёт уже не в человеко-годах.

Итог

Формальная верификация перестала быть искусством для авионики. Claude закрыл доказательствами 239 точек входа в 123 библиотеках, нашёл по дороге баги, которые не всплывали после триллионов прогонов, и сделал это на уровне машинного кода, не требуя переписать ни строки. Ограничения серьёзные: RISC-V вместо x86, однопоточность, многословный стиль доказательств и вечный вопрос о совпадении спецификации с реальностью.

Но направление понятно. Если стоимость доказательства падает на 40% за поколение моделей, а доказательства переиспользуются как библиотечный код, то лет через пять вопрос будет звучать не «зачем верифицировать», а «почему у вашей зависимости в CI нет доказательства». Начать можно сегодня: посмотреть опубликованные доказательства и семантики, прогнать пайплайн Theorem на своей библиотеке или просто дать Claude задачу доказать, что ваш фаззинг-тест не падает никогда.