Claude доказал отсутствие сбоев в 239 тестах OSS-Fuzz — но с важной оговоркой
Claude доказал отсутствие сбоев в 239 тестах OSS-Fuzz — но с важной оговоркой
Обычный фаззинг ищет сбой, перебирая множество входов. Anthropic и компания Theorem предложили другой ход: превратить существующий тест в математическое утверждение и попросить Claude построить к нему доказательство. За несколько недель система исправила найденные ошибки и доказала отсутствие сбоев на входах до 64 МБ для 239 тестовых точек в 123 библиотеках из Google OSS-Fuzz.
Практический смысл здесь не в красивом слове «доказано». Если утверждение верно, для конкретной тестовой точки больше не нужно надеяться, что генератор входов когда-нибудь наткнётся на падение: доказательство охватывает все входы заданного размера. Это может сделать проверку общих зависимостей менее похожей на бесконечную лотерею.
Как тест превращают в доказательство
Авторы берут компилируемый фазз-тест и собирают его в RISC-V-бинарник. Затем формальная модель процессора и Linux превращает требование «тест не падает» в спецификацию. Claude пишет доказательство, а ядро Rocq проверяет его независимо от модели.
В опубликованном эксперименте это дало около 180 млн строк доказательств Rocq. Типичное доказательство занимает примерно 600 тыс. строк и относится к бинарнику медианной длиной 18 тыс. инструкций RISC-V. Часть артефактов Anthropic и Theorem выложили, чтобы их можно было перепроверить и использовать повторно.
График: Anthropic.
Не «в библиотеке нет багов»
Это как раз ключевое ограничение, которое легко потерять в пересказе. Доказательства относятся к однопоточным статическим RISC-V-бинарникам с фиксированным бюджетом памяти и моделью Linux. Большинство реальных пользователей запускают эти библиотеки на x86 или ARM, часто с динамической glibc — это другой мир исполнения.
Кроме того, доказан только выбранный набор свойств тестовой точки: отсутствие сбоев, включая проверяемые AddressSanitizer случаи. AddressSanitizer не ловит все ошибки памяти, не все входы каждой библиотеки были покрыты, а программа-вызовник тоже может использовать библиотеку неправильно.
И всё же это заметный сдвиг для разработчиков: LLM здесь выступает не как «авторитетный ревьюер», а как дорогой генератор формального артефакта, который затем проверяет отдельный механизм. Самая честная формула результата: не гарантия безошибочного ПО, а способ сузить область недоверия до спецификации, модели машины и проверяющего ядра.
