Формальная верификация кода с Claude, доказательства для 123 открытых библиотек
Frontier Red Team из Anthropic поручила Claude формально доказать, что программы не падают. За несколько недель Claude доказал это для 239 точек входа в 123 библиотеках и попутно нашёл сотни багов.
Что сделали
Команда превратила существующие фаззинг-тесты OSS-Fuzz в спецификации. Требование одно, скомпилированный под RISC-V бинарник не падает ни на одном входе меньше 64 МБ. На основе семантики RISC-V и Linux от Theorem Claude писал доказательства на Rocq, а проверял их отдельный proof checker. Если доказательство упиралось в баг, Claude исправлял код, спецификацию генерировали заново, а Claude продолжал. За патчи давали штраф, а сами патчи проверяли на reward hacking.
Что получилось
За несколько недель Claude доказал отсутствие падений для 239 точек входа в 123 библиотеках, это около 180 миллионов строк на Rocq. Попутно он нашёл сотни багов. Доказательства покрывают только однопоточные статически собранные бинарники под RISC-V.
На что обратить внимание
Одно доказательство может стоить сотни миллионов токенов. В тесте из 36 задач агенты с возможностью копировать доказательства друг друга тратили на 17% меньше токенов.
Пояснение
Формальная верификация математически доказывает свойство программы для всех входов, а не проверяет отдельные примеры, как тесты. Rocq (бывший Coq) это система для записи и проверки таких доказательств. OSS-Fuzz это проект Google, где открытые библиотеки постоянно прогоняют через фаззинг, то есть через случайные входные данные. Reward hacking это когда модель выполняет задачу формально, обходным путём, а не по существу.
Кому пригодится
Инженерам по безопасности и мейнтейнерам открытых библиотек, если тестов и фаззинга мало и нужны гарантии.
Попробуйте сами с Claude
Хочу формально доказать, что [модуль или библиотека в моём коде и путь к ней] свободна от [класс багов, например выход за границы массива или переполнение целых]. Выбери подходящий инструмент верификации для [язык], напиши спецификации и доказательства и запусти их. В конце дай отчёт о том, что доказано, что не получилось и какие баги нашлись. Не меняй мой исходный код, пока не покажешь мне diff.
Нужна помощь с запуском? Вступайте в сообщество AI Pack ↗
Источник: anthropic.com ·