Claude написал 180 млн строк доказательств, проверяя безопасность реального ПО.

Anthropic и Theorem показали подход, который превращает фаззинг-тесты в математические гарантии.

Обычный фаззер перебирает огромное количество входных данных и ищет сбой. Но даже триллионы запусков не гарантируют, что опасный случай найден.

Здесь Claude получает другую задачу: доказать, что выбранный тест не упадёт ни на одном входе размером менее 64 МБ - в рамках заданной модели исполнения.

За несколько недель удалось построить доказательства для 239 точек входа в 123 open-source библиотеках. Проверка идёт на уровне скомпилированного кода RISC-V: Claude пишет доказательство, а Rocq проверяет его корректность.

В процессе обнаружились сотни ошибок. Например, выход за границы памяти в распаковщике, требовавший входа около 20 МБ с редкой структурой.

Это не гарантия отсутствия всех багов в библиотеках. Доказательства покрывают конкретные точки входа и условия: однопоточный статический бинарник, ограниченную память и формальную модель RISC-V/Linux.

Но результат показывает перспективу: вместо бесконечного поиска контрпримеров — проверяемое доказательство конкретного свойства программы.

https://www.anthropic.com/research/formal-verification