Claude написал 180 млн строк доказательств для проверки безопасности реального ПО.
Что произошло
Claude написал 180 миллионов строк доказательств, проверяя безопасность реального ПО. Anthropic и Theorem показали подход, который превращает фаззинг-тесты в математические гарантии.
Обычный фаззер перебирает огромное количество входных данных и ищет сбой. Но даже триллионы запусков не гарантируют, что опасный случай найден.
Claude получил другую задачу: доказать, что выбранный тест не упадёт ни на одном входе размером менее 64 МБ в рамках заданной модели исполнения.
За несколько недель удалось построить доказательства для 239 точек входа в 123 open-source библиотеках. Проверка идёт на уровне скомпилированного кода RISC-V: Claude пишет доказательство, а Rocq проверяет его корректность.
В процессе обнаружились сотни ошибок. Например, выход за границы памяти в распаковщике, требовавший входа около 20 МБ с редкой структурой.
Это не гарантия отсутствия всех багов в библиотеках. Доказательства покрывают конкретные точки входа и условия: однопоточный статический бинарник, ограниченную память и формальную модель RISC-V/Linux.
Мы видим в этом важную перспективу: вместо бесконечного поиска контрпримеров появляется проверяемое доказательство конкретного свойства программы.
Ещё новости:
