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

Трансляция фаззинга в математические спецификации на базе RISC-V

Классическая верификация требует огромных ресурсов: создание микроядра seL4 заняло два человеко-года, тогда как его математическое доказательство потребовало двадцати человеко-лет экспертного труда. Anthropic и Theorem изменили правила игры, автоматизировав трансляцию тестов из репозитория Google OSS-Fuzz в строгие математические формулировки. Программный код библиотек компилировался в исполняемые бинарные файлы архитектуры RISC-V. Задача формулировалась на базовом системном уровне: гарантировать, что приложение при любых входных данных объемом до шестидесяти четырех мегабайт завершит работу штатно, без повреждений памяти, ошибок адресного санитайзера и падений утверждений.

Для двухсот тридцати девяти входных точек в ста двадцати трех библиотеках Claude сгенерировал в совокупности около ста восьмидесяти миллионов строк доказательного кода на специализированном языке Rocq. При этом средний объем файла верификации для отдельного бинарника составлял порядка шестисот тысяч строк. Ключевое достоинство архитектуры заключается в устранении проблемы нейросетевых галлюцинаций. Человеку и службе безопасности не требуется слепо доверять коду, сгенерированному языковой моделью. Результат Claude передается независимому строгому ядру верификации Rocq. Доверенная база сжимается всего до трех компонентов: формальной семантики инструкций RISC-V и процессов операционной системы Linux, текста самого математического утверждения и непосредственно исполняемого файла верификатора Rocq.

Ликвидация скрытых дефектов за пределами возможностей динамического анализа

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

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

Экономика вычислений и масштабирование на промышленные инфраструктуры

Главным барьером на пути внедрения ИИ-верификации остается вычислительная стоимость синтеза сотен миллионов токенов. Однако результаты Anthropic демонстрируют экспоненциальную динамику удешевления процессов. При решении контрольного набора из тридцати шести задач верификации архитектура Opus 5.5 потребовала на сорок процентов меньше токенов по сравнению с Opus 5. Дополнительный скачок эффективности обеспечивает организация совместной работы мультиагентных систем. Подобно тому как сообщество проекта Mathlib в среде Lean повторно использует миллионы формализованных лемм, агенты Claude переиспользовали базовые фрагменты верификации инициализации рантайма языка Си и санитайзеров, что снизило совокупные затраты вычислительных мощностей еще на семнадцать процентов.

Эксперименты вышли далеко за пределы RISC-V. Исследователи успешно доказали корректность реализации алгоритма сжатия zlib из состава ядра Linux непосредственно на бинарном коде x86 в полном соответствии со стандартом RFC 1950, а также провели кросс-верификацию интерпретатора Python, написанного на Rust, подтвердив его семантическую идентичность эталонному CPython на выборке из почти двух миллионов синтетических программ. Следующим шагом Theorem заявляет верификацию корневой инфраструктуры дистрибутива Nix, включая системную библиотеку glibc, стек OpenSSL и утилиту cURL.

Границы применимости и вектор трансформации разработки

Несмотря на технологический триумф, авторы подчеркивают принципиальную разницу между формально верифицированным и абсолютно безошибочным кодом. Математическое доказательство гарантирует истинность поведения только внутри заданной модели. Текущие эксперименты опирались на упрощенную семантическую модель статических однопоточных бинарных файлов под управлением библиотеки musl. Реальные же серверные среды функционируют в многопоточном режиме, полагаются на сложную динамическую компоновку glibc и выполняются на конвейерах x86 и ARM со сложным внеочередным исполнением команд и специфическими моделями памяти.

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