Formalizing CPython

The project uses AI agents to translate CPython - the C implementation that defines how Python behaves in practice - into Lean, a language whose proofs are checked by computer. Each translated function follows the original code closely, including error handling and low-level details such as C’s wrapping arithmetic. The team compares each copy with real Python on at least 50,000 difficult inputs, proves meaningful properties about it, and has a separate agent review the work. This strict process matters because a mathematically valid proof can still be useless if it also applies to a broken function, or misleading if the Lean copy does not match real Python.

So far, 4,071 functions have passed review, comprising 613,318 lines of Lean and 18,898 checked theorems and lemmas. The work covers portions of CPython 3.15.2, with progress ranging from 9% of the standard library to all grammar rules. It has also produced 418 bug reports, including mismatches between C and Python implementations, incorrect results, crashes, and memory corruption; roughly 55 issues can crash the interpreter or corrupt memory through ordinary Python code. Testing against real Python exposed mistakes the proofs alone could not catch, such as overlooked memory-allocation failures and assumptions about startup behavior. The account argues that formalization can make CPython’s obscure behavior precise and uncover bugs, while showing that AI-generated proofs require rigorous testing and independent review to be trustworthy.