Anthropic и Theorem использовали Claude для доказательства свойств безопасности 123 библиотек

22 октября 2026 года Anthropic рассказала о совместном исследовании с Theorem: Claude использовали для построения формальных доказательств свойств безопасности программ. Работа охватила 239 тестовых точек входа в 123 библиотеках из OSS-Fuzz. Это исследовательский результат, а не новая версия модели или универсальная гарантия надёжности библиотек.

Как проверяли результат

Обычное тестирование перебирает конкретные входные данные. Здесь существующие тесты превращали в математические требования к скомпилированной программе. Claude писал доказательства, а их соответствие требованиям проверяло ядро системы Rocq. Таким образом, итог проверяется отдельным инструментом, а не принимается на веру из ответа нейросети.

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

Что открыли и чего не доказали

В опубликованной части репозитория на момент проверки представлены доказательства для 60 точек входа в 25 библиотеках. Это меньше общего масштаба исследования. Материалы позволяют независимо проверять и изучать подход.

Авторы отдельно предупреждают: доказательство не означает отсутствие любых ошибок во всей библиотеке, не переносится автоматически на x86-64 и не гарантирует отсутствие бесконечных циклов. Корректность формальной модели исполнения и самого проверяющего инструмента также остаётся важным условием.

Редакционный вывод: для команд разработки ценность подхода в проверяемых гарантиях с явно указанными границами. Это возможное дополнение к тестам и аудиту, но не повод отменять их или считать весь проект безопасным.

Источники: Anthropic, 22 октября 2026 года; репозиторий доказательств Theorem, проверен 23 октября.