Anthropic: Claude превратил тесты OSS-Fuzz в проверяемые доказательства

Anthropic вместе с Theorem показали более узкий, но практичный сценарий для Claude: не «проверить библиотеку целиком», а взять 239 входов OSS-Fuzz в 123 open-source библиотеках и для них построить формальную проверку того, что в заданных условиях не возникает crash. Подход опирается на генерацию доказательств в Rocq для собранных RISC-V бинарников, после чего эти доказательства независимо принимает проверяющее ядро Rocq. Подробности — в исследовании Anthropic: formal verification.

Масштаб заметный: успешные прогоны дали около 180 млн строк доказательств. Но трактовать это как «Claude верифицировал 123 библиотеки» нельзя. Охват ограничен конкретными точками входа, входами меньше 64 МБ и фиксированной средой исполнения: Linux, однопоточная статическая сборка и заданный бюджет памяти.

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