ИИ-модели сделали формальную проверку открытого кода массовой: Anthropic доказала свойства в 123 библиотеках

Claude доказал свойства безопасности в скомпилированном коде 123 библиотек из OSS-Fuzz и нашёл баги, которые годами никто не замечал.

Не хотите разбираться сами? Внедряем ИИ в ваш бизнес: задачи без лимита, одна цена в месяц, отмена в любой момент.

Что проверено. В заявке 239 точек входа в 123 библиотеки. В публичный репозиторий oss-verify-proofs выложено 60 точек входа в 25 библиотеках: zlib, LZO, libexpat, cpp-httplib, libcups, freerdp и libzmq. Доказанная модель Python-парсера совпадает с CPython в 99,95% случаев на 1,7 млн тестов.

Чем это проверено. Доказательства пишутся на Rocq, и принимает их сам ассистент доказательств, а не текст модели. Типичное доказательство около 600 тысяч строк, медианный бинарник около 18 тысяч инструкций RISC-V.

Экономика. Opus 5.5 доказал половину задач с расходом токенов на 40% меньше, чем Opus 5. Переиспользование доказательств экономит ещё 17% токенов.

Повторить. Клонируете oss-verify-proofs, выполняете ./oft fetch coturn, ставите зависимости из tools/oft/requirements.txt и запускаете образ ghcr.io/theorem-labs/oss-fuzz-theorems-checker командой ./oft check coturn/FuzzStunClient --parts statements,proofs. Образ работает с --network none. Нужны Rocq 9.2.0, Python 3 с PyYAML и до 20 ГБ памяти на 16 ядрах.

Свою библиотеку в репозиторий добавляют через PR по семи шагам из SKILL.md add-project.