Formalizing CPython

Researchers used AI agents to formalize 613,318 lines of CPython's C code into Lean, a language for machine-checked proofs, discovering 418 bugs in the process, including about 55 critical ones that can crash the interpreter or corrupt memory. By forcing precise definitions of what code does in all edge cases, the formal verification process revealed gaps between CPython's actual behavior and what developers assumed it would do. So far, 4,071 functions have been formally verified and accepted through independent review.