Claude нашёл сотни багов, доказывая правильность чужого кода

Claude — это модель ИИ от Anthropic. Чтобы проверить код, написанный другими, они использовали Claude для проверки корректности ~123 open source библиотек в OSS-Fuzz (постоянном проекте Google по фаззинг-тестированию open source софта). Вместе со своими партнёрами по формальной верификации из Theorem они сгенерировали ~180 млн строк формальных доказательств верификации, выраженных на языке проверки доказательств Rocq. Каждое доказательство проверялось независимо с помощью другого инструмента. В процессе Claude нашёл и исправил сотни давних багов. Эти доказательства не являются универсальными — они применимы к однопоточной среде выполнения, архитектуре набора команд RISC-V и файлам меньше 64 МБ.

Если ты из тех, кто использует ИИ-агентов для работы с реальным кодом, это гораздо интереснее, чем очередной результат бенчмарка. Проверка корректности кода часто становится узким местом в рабочем процессе. Сама генерация кода не такая уж сложная задача. В этом случае перед Claude стояла задача проверить код, который он сам не писал. Это не заменяет код-ревью, потому что результаты верны только при определённых ограничениях. Но мы движемся к будущему, где ИИ-агенты смогут не просто предлагать автодополнения, а генерировать и проверять код.