Anthropic применила Claude для формальной проверки 123 библиотек из OSS-Fuzz

Anthropic и компания Theorem с помощью Claude сгенерировали около 180 млн строк формальных доказательств для 239 тестовых точек входа в 123 библиотеках с открытым кодом. Проверка также выявила сотни ошибок, однако полученные гарантии действуют только в рамках заданной модели исполнения.

Anthropic сообщила о крупном эксперименте по автоматизации формальной проверки программного обеспечения с помощью языковой модели Claude. Совместно со специализирующейся на верификации компанией Theorem исследователи проверили 239 точек входа в 123 библиотеках проекта Google OSS-Fuzz.

Claude преобразовывал условия фаззинг-тестов в математические утверждения и создавал доказательства на языке системы Rocq. За несколько недель модель сгенерировала около 180 млн строк доказательств, которые автоматически проверялись ядром Rocq. В процессе Claude обнаружил сотни ошибок, в том числе дефекты, остававшиеся незамеченными в течение многих лет, и в ряде случаев подготовил исправления.

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