Anthropic сообщила, что Claude сгенерировал математические доказательства корректности существующего кода для 123 библиотек с открытым исходным кодом. Объём созданного доказательного кода составил примерно 180 млн строк.
В ходе работы модель обнаружила ошибки, которые, согласно описанию The Decoder, не выявили годы тестирования. Anthropic ставит целью сделать формальную верификацию с помощью ИИ такой же привычной практикой, как стандартное тестирование.
Практическое значение зависит от того, насколько независимо подтвердятся эти результаты и насколько применим подход к другим проектам. В представленном пакете есть только синопсис публикации, а не её полный текст или отдельные доказательства.
комментарий редакции
Что это значит
Вероятное следствие — усиление интереса к ИИ-инструментам формальной проверки кода, если результаты подтвердятся. Следующим наблюдаемым сигналом станет независимая оценка доказательств и реакция разработчиков библиотек. Существенная неопределённость связана с отсутствием в пакете первичных материалов и подробностей об обнаруженных ошибках.
Дополнительные оценки
Ollama Cloud
GLM 5.2
Заявление Anthropic о генерации ~180 млн строк доказательного кода для 123 библиотек потенциально сдвигает ИИ-верификацию из академической ниши в инженерную практику, но единственный источник без первичных данных Anthropic не позволяет оценить реальную глубину результата. Наблюдаемый следующий сигнал — независимая оценка доказательств специалистами по формальным методам и реакция мейнтейнеров затронутых библиотек. Существенная неопределённость связана с отсутствием информации о том, какие именно ошибки найдены, какова доля принятых доказательств и применим ли подход за пределами отобранных проектов.
В чём оценки сходятся- Канонический анализ правомерно отмечает, что практическое значение зависит от независимого подтверждения и переносимости подхода на другие проекты.
- Согласен, что источник в виде краткого синопсиса без первичного заявления Anthropic недостаточен для окончательной оценки масштаба и качества результата.
- Корректно зафиксировано расширение роли ИИ: от генерации кода к формальному доказательству корректности — это качественно новый шаг.
- Стратегический вывод о вероятном усилении интереса к ИИ-формальной верификации может быть преждевременным: одно заявление без подтверждённых деталей редко меняет отраслевые практики.
- Утверждение о найденных ошибках, пропущенных годами тестирования, требует осторожности: формулировка The Decoder не уточняет серьёзность и реальное влияние этих багов.
- Отсутствие в пакете списка библиотек и типов доказательств — не просто пробел, а ключевое ограничение: без него невозможно судить, репрезентативна ли выборка для широких выводов.
Ollama Cloud
Kimi K2.6
Заявленный результат — значимый маркер возможного перехода ИИ от генерации кода к его формальному доказательству корректности, что при успешном масштабировании изменит экономику обеспечения качества ПО. Следующим критическим сигналом станет публикация независимыми исследователями или мейнтейнерами библиотек подтверждения корректности сгенерированных доказательств и реальности выявленных ошибок. Существенная неопределённость заключается в отсутствии первичных данных: 180 млн строк доказательного кода могут содержать как прорывные результаты, так и формально корректные, но практически бесполезные конструкции, а «ошибки, пропущенные годами тестирования», требуют верификации на уровне конкретных CVE или публичных репортов.
В чём оценки сходятся- Масштаб заявленного применения формальной верификации к 123 библиотекам действительно указывает на потенциальный сдвиг в практике разработки ПО.
- Отсутствие в пакете первичных материалов Anthropic и независимой верификации снижает достоверность оценки качества результатов.
- Практическая ценность подхода напрямую зависит от переносимости на проекты с иной архитектурой и спецификацией.
- Канонический анализ недостаточно подчёркивает риск «proof bloat»: 180 млн строк на 123 библиотеки (~1,5 млн строк на библиотеку) намекают на возможную генерацию шаблонных или избыточных конструкций, а не на глубокие доказательства.
- Формулировка «ошибки, пропущенные годами тестирования» без уточнения критичности может создавать ложное впечатление о превосходстве формальной верификации: найденные баги могли быть маргинальными или находиться в нетестируемых спецификациях.
- Стратегический вывод о «усилении интереса» избыточно осторожен: при подтверждении результатов это скорее запускает гонку за интеграцию ИИ-верификации в CI/CD, а не постепенное нарастание интереса.