Claude научился математически проверять программы на ошибки В... - Vibeus

Pavel K · 2026-10-23

Claude научился математически проверять программы на ошибки

В Anthropic поручили Claude проверить 123 библиотеки открытого кода. Вместо привычного перебора тестов модель написала математические доказательства того, что определённые участки программ не завершатся аварийно при заданных условиях. Их корректность проверяла отдельная система Rocq.

Попутно Claude обнаружил сотни ошибок. Одна из них пряталась в распаковщике данных и проявлялась только на файлах около 20 МБ с редкой структурой.

Доказательства пока действуют для специальных сборок под RISC-V, а не для всех версий этих программ.

https://www.anthropic.com/research/formal-verification