Formalizing CPython

Formalizing CPython AI agents wrote 613,318 lines of Lean that copy Python's internals line by line, tested every piece against the real Python, had a computer check every proof, and turned up 418 bug reports in Python along the way. David Andrews and Chao Zhang 9 November 2026 Code and data CPython · Objects/rangeobject.c static unsigned long get_len_of_range ( long lo, long hi, long step) { assert(step != 0 ); if (step > 0 && lo < hi) return 1UL + (hi - 1UL - lo) / step; else if (step < 0 && lo > hi) return 1UL + (lo - 1UL - hi) / ( 0UL - step); else return 0UL ; } Lean copy · RangeSlice/Model.lean def getLenOfRange (lo hi step : Int ) : Int := if step > 0 ∧ lo < hi then uadd 1 ( usub ( usub ( toU hi) 1 ) ( toU lo) / toU step) else if step < 0 ∧ lo > hi then uadd 1 ( usub ( usub ( toU lo) 1 ) ( toU hi) / usub 0 ( toU step)) else 0 -- step ≠ 0 is assumed by every proof -- uadd, usub: C's unsigned arithmetic, -- which wraps around past 2^64 TL;DR We pointed Opus 5.5 at CPython, the program that runs almost all Python code, and had it rewrite its functions in Lean , a language for writing machine-checked proofs. Each rewrite copies the original line by line and is tested against real Python on tens of thousands of inputs before anyone tries to prove anything about it. A function only counts once a second agent, which didn't write it, checks the work and agrees it holds up. 4,071 functions have passed that check so far. The result is 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. Along the way the proofs turned up 418 bug reports. Most are small, but about 55 can crash the interpreter or corrupt memory from ordinary Python code. Checked and accepted Written, not yet accepted Not started All of CPython 16% Interpreter core 10% Built-in types 35% C modules 19% Parser 31% Grammar rules 100% Standard library 9% Why bother Python doesn't have a precise written definition. There is a reference manual, but in practice "Python" means whatever CPython does, and CPython is hundreds of thousands of lines of C plus a large standard library. The manual covers normal use. It says little about the odd cases, and that's where bugs hide: an object that changes a dictionary while that dictionary is searching for it, an error thrown halfway through an update, a number one past the largest the C code was written for. Writing a proof about a function forces you to say exactly what it does in all of those cases. You can't leave anything vague, because the proof checker won't accept it. That makes proofs a good way to find the places where the code doesn't do what everyone assumes. We wanted to see how far this goes on a code base as large and old as CPython, and whether the results stay trustworthy when most of the work is done by AI. How it works Every function goes through the same four steps. Copy Rewrite the function in Lean, following the original code line by line, including its error messages and its odd corners. Test Run the copy and the real Python side by side on at least 50,000 tricky inputs. Any disagreement means the copy is wrong. Prove State something that should always be true and have the computer check the proof. If it's actually false, prove that instead. Check A second agent that didn't do the work reviews it against the original and tries to break it. Only what survives counts. The code at the top of this page is step one for a small piece of CPython: the C function that works out how many numbers are in a range , next to its Lean copy. The copy keeps the C code's exact arithmetic, including how its numbers wrap around when they get too big. The proof about it shows that this function, the slower version CPython uses for very large numbers, and the code that chooses between them always give the same, correct count. Proofs that prove nothing The hardest part wasn't getting AI agents to write proofs. It was getting proofs that actually mean something. Our first attempt asked the agents for breadth: copy every function and prove at least one thing about each. They did. Then a separate review found that fewer than half of the functions it checked held up, and in one file only 21%. The proofs were all correct. They just didn't say anything useful. For example, "if this function returns a number, the number is at least zero" is true, but a function that always crashes also satisfies it. So the reviewer now asks one question about every proof: could a broken version of the function pass it too? Version of the function "If it returns, the answer is ≥ 0" "It always returns the right count" The real one passes passes Always crashes passes caught Returns 0 for very large numbers passes caught Off by one when counting down passes caught Fixing a weak proof usually means going back and making the copy more realistic, for example letting a user's code throw an error in the middle of a function. The charts below show how that went for ten files. Each point is one round of review. The lines sometimes go down: when a reviewer finds that an accepted proof is wrong about real Python, everything that relied on it is taken back out. Functions accepted 100% 0% review 1 review 5 review 1: 0 of 142 accepted review 2: 2 of 142 accepted review 3: 41 of 142 accepted review 4: 130 of 142 accepted review 5: 135 of 142 accepted 100% 0% review 1 review 5 review 1: 1 of 56 accepted review 2: 18 of 56 accepted review 3: 54 of 56 accepted review 4: 55 of 56 accepted review 5: 56 of 56 accepted 100% 0% review 1 review 7 review 1: 31 of 46 accepted review 2: 42 of 46 accepted review 3: 44 of 46 accepted review 4: 45 of 46 accepted review 5: 44 of 46 accepted review 6: 45 of 46 accepted review 7: 46 of 46 accepted 100% 0% review 1 review 5 review 1: 31 of 48 accepted review 2: 39 of 48 accepted review 3: 42 of 48 accepted review 4: 43 of 48 accepted review 5: 45 of 48 accepted 100% 0% review 1 review 9 review 1: 21 of 39 accepted review 2: 30 of 39 accepted review 3: 35 of 39 accepted review 4: 34 of 39 accepted review 5: 33 of 39 accepted review 6: 34 of 39 accepted review 7: 29 of 39 accepted review 8: 36 of 39 accepted review 9: 37 of 39 accepted 100% 0% review 1 review 3 review 1: 11 of 38 accepted review 2: 31 of 38 accepted review 3: 37 of 38 accepted 100% 0% review 1 review 2 review 1: 9 of 43 accepted review 2: 41 of 43 accepted 100% 0% review 1 review 2 review 1: 19 of 33 accepted review 2: 33 of 33 accepted 100% 0% review 1 review 2 review 1: 14 of 33 accepted review 2: 31 of 33 accepted 100% 0% review 1 review 2 review 1: 29 of 40 accepted review 2: 35 of 40 accepted Rounds of review → When a correct proof is wrong anyway A checked proof guarantees that a statement follows from the copy. It doesn't guarantee the copy matches real Python, and testing only covers the inputs you thought to try. So every accepted statement is also run against real Python. That caught several proofs that were valid and still wrong. The 16-terabyte string The copy of Python's fast JSON encoder assumed memory requests always succeed. So it "proved" the encoder could build its indentation strings for any nesting depth, including one that needs 16 terabytes of memory. Real Python runs out of memory. The fixed copy now treats every memory request as something that can fail. Nine extra steps, just once A proof said Python's pickle module never goes deeper than a certain number of nested calls. That turned out true except in a brand-new Python process. There, the first time it encodes a string, it quietly loads a text codec, and that load uses nine more nested calls. Our tests never saw it, because the test harness had already loaded the codec. Error types have famili