Formalizing CPython
Summary
David Andrews and Chao Zhang describe an AI-assisted effort to formalize CPython in Lean by translating its C internals line by line, testing against real Python, and proving properties with Lean. The project has produced 613,318 Lean lines across 1,539 files, 18,898 theorems, and 418 bug reports, illustrating both the promise and challenges of machine-checked proofs on a large, long-standing codebase.