Anthropic: LLM делают формальную верификацию ПО осуществимой в гораздо большем масштабе
Anthropic
Claude написала доказательства на Rocq на уровне ассемблера RISC-V для 239 точек входа OSS-Fuzz в 123 open-source библиотеках — примерно 180 млн строк доказательств, — установив, что бинарники никогда не падают на входных данных меньше 64 МБ в рамках смоделированной модели памяти Linux. Работа выявила сотни багов, включая повторное обнаружение CVE-2026-56132 в libexpat, а сопутствующий эксперимент проверил собранный Claude интерпретатор Python на Rust против CPython на более чем 1,7 млн программ с совпадением 99,95%.
Почему это важно
Это первая крупномасштабная демонстрация машинно-проверенных доказательств, написанных ИИ, на production-коде, причём гарантии явно обусловлены спецификациями и однопоточной моделью RISC-V, а не означают полностью безбаговое ПО.
Важность: 4/5
первая крупномасштабная формальная верификация production-кода, написанная ИИ