David Andrews uses AI agents to build Lean model of CPython
The gist
David Andrews' AI-written Lean model of CPython 3.15.2 spans 613,318 lines and 18,898 theorems.
It found 418 bug reports, about 55 of them crashes reachable from Python code.
How it unfolded
- Oct 22, 2026Anthropic reported asking Claude to build a Rust interpreter for a large subset of Python and prove with Verus that it matches CPython semantics, finding identical behavior in 99.95% of over 1.7 million randomly generated programs.
- Nov 9, 2026David Andrews and Chao Zhang published "Formalizing CPython: A Lean Model of CPython 3.15.2," reporting AI agents wrote 613,318 lines of Lean across 1,539 files with 18,898 theorems and lemmas, all checked by Lean's proof checker on every build.
- Nov 9, 2026The write-up reported 4,071 functions through independent review, 3,834 properties proved and 588 refuted, and 418 bug reports with reproducers, about 55 of them crashes or memory errors reachable from Python code.
Key terms
- Lean
- Formal proofs written in Lean, a proof assistant and functional programming language.
- theorems
- A statement in mathematics or formal logic that has been proven, or can be proven, by logical argument from axioms and earlier theorems.
Source: Wikipedia