AI agents rewrote CPython code in Lean to find bugs

The authors of the Formalizing CPython project used autonomous AI agents to rewrite the interpreter's source code into the Lean interactive theorem prover language. During the process, the systems processed 613,318 lines of the CPython codebase.

In the course of automated testing and mathematical correctness proofs, the agents identified 418 bugs. Among the discovered vulnerabilities and programming errors, 55 defects were recorded that are guaranteed to cause a crash or failure of the interpreter.

The project demonstrates the practical applicability of formal verification methods combined with generative models for finding critical bugs in large-scale industrial software written in C.