AI-агенты переписали код CPython на Lean для поиска багов

Авторы проекта Formalizing CPython применили автономные AI-агенты для переписывания исходного кода интерпретатора на язык интерактивного доказательства теорем Lean. В ходе работы системы обработали 613 318 строк кодовой базы CPython.

В процессе автоматизированного тестирования и математического доказательства корректности агенты выявили 418 багов. Среди найденных уязвимостей и ошибок программирования зафиксировано 55 дефектов, которые гарантированно приводят к аварийному завершению работы или падению интерпретатора.

Проект демонстрирует практическую применимость формальных методов верификации в сочетании с генеративными моделями для поиска критических ошибок в масштабном промышленном ПО, написанном на C.