Formalizing CPython An AI agent built on Opus 5.5 rewrote CPython's functions in Lean, producing 613,318 lines of machine-checked Lean across 1,539 files with 18,898 theorems and lemmas, and surfaced 418 bug reports in Python — about 55 of which can crash the interpreter or corrupt memory from ordinary Python code. Each Lean rewrite copies the original C line by line and is tested against real Python on tens of thousands of inputs before proving, and a function only counts once a second agent that didn't write it verifies the work; 4,071 functions have passed that check. The effort targets the absence of a precise written definition of Python, since proofs force exact specification of edge cases where CPython's C implementation diverges from assumptions. 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. 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 https://lean-lang.org , 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. 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. 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. 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 families In Python, catching a TypeError also catches any more specific error built on top of it. Three separate copies checked an error's exact name instead. All three had proofs that a custom error type could break. Memory that comes back The copy of Python's set assumed that once memory is freed, the same address never comes back. Real memory allocators reuse addresses all the time. CPython uses a "did the address change?" check to notice when user code has swapped out the set's internals. With reuse, that check can be fooled. Fixing the copy turned an accepted proof into a real memory bug, now one of our bug reports. What we found When a proof fails because Python itself is wrong, and not the copy, we write it up as a bug report. Each report includes a short script that shows the bug on Python 3.15.2 for most, also on the development version , a search for duplicates already reported, and an honest rating of how much it matters. Most are small: an error message that's wrong, an edge case that behaves differently from the documentation, two versions of a function that disagree. About 55 are more serious and can crash Python or corrupt its memory using nothing but normal Python code, usually by having user code change a container while C code is in the middle of using it. Python doesn't treat running hostile Python code as a security boundary, so these are ordinary bugs. The ones not already on CPython's tracker are being reported to the project, starting with this post. Six small examples of different kinds: A dictionary call that crashes Python Calling setdefault on an object's attribute dictionary with a StrEnum key crashes the interpreter, if another object of the same class has that attribute and this one doesn't. class Key StrEnum : NAME = "name" class User: pass a = User ; a.name = "ada" b = User ; b.age = 36 vars b .setdefault Key.NAME, "anon" Segmentation fault An XML edit that corrupts memory Assigning to a backwards slice of an ElementTree element should insert, as it does for a list. Instead it duplicates one child without taking a reference and loses another. e = ET.Element "root" e : = ET.Element f"a{i}" for i in range 7 e 5:2 = ET.Element "X" c.tag for c in e 'a2' appears twice, 'a4' is gone An email header that breaks the parser A Message-ID with a space inside square brackets makes Python's email parser fail with an internal error. The header comes from whoever sent the email. msg = email.message from string "Message-ID: