AI-written Lean formalization of CPython surfaces 418 bug reports

What happened

A project that surfaced on the Hacker News front page has used AI agents to translate CPython, the implementation that runs nearly all Python code, into Lean, a language for machine-checked proofs. According to the project write-up on broyojo.com, the team pointed the Opus 5.5 model at CPython 3.15.2 and had agents rewrite its internal functions in Lean, then prove properties about them.

The output so far: 613,318 lines of Lean across 1,539 files, containing 18,898 theorems and lemmas, all verified mechanically by Lean's proof checker on every build. Some 4,071 functions have passed an adversarial review by a second agent. Along the way, the work generated 418 bug reports against Python, of which roughly 55 describe flaws that can crash the interpreter or corrupt memory using ordinary Python code.

How each function is handled

Every function goes through four stages, per the write-up. First it is copied: rewritten in Lean while tracking the original C or Python closely, including error messages and quirks such as unsigned arithmetic wrapping past 2^64. Then it is tested: the Lean model runs side by side with real Python on at least 50,000 deliberately tricky inputs, and any disagreement means the model is wrong. Next it is proved: agents state something that should always hold and have the computer check the proof, or, if the claim turns out to be false, prove that instead. Finally, a separate agent that did none of the writing reviews the result against the original and tries to break it; only what survives is counted.

Coverage varies widely by area. Grammar rules are complete, while the parser stands at 31 percent, built-in types at 35 percent, C modules at 19 percent, the interpreter core at 10 percent and the standard library at 9 percent, for 16 percent of CPython overall. Code with nothing meaningful to verify, such as memory bookkeeping, is excluded from the tally.

When correct proofs say nothing

The project's hardest problem was not getting agents to write proofs, but writing proofs that mean anything. An early attempt asked for breadth, with at least one proof per function, and the agents delivered. A subsequent review found that fewer than half of the functions it examined held up, and only 21 percent in one file. The proofs were all soundly checked; they were just trivially true. A statement like "if this function returns a number, the number is at least zero" is satisfied just as well by a function that always crashes.

The fix was a sharper review criterion: for every proof, ask whether a broken version of the function could also satisfy it. If so, the proof is rejected, and the copy is usually made more realistic, for example by allowing user code to raise an error partway through a function.

Acceptance climbs over rounds of review but is not monotonic. Objects/genobject.c went from 1 of 56 functions accepted to 56 of 56 in five rounds; Objects/typeobject.c reached 135 of 142 in five; Objects/setobject.c needed seven. When a reviewer discovers an accepted proof mischaracterizes real Python, everything that relied on it is pulled back out.

The gap a checker cannot close

A verified proof guarantees only that a statement follows from the Lean copy; it cannot guarantee the copy matches actual CPython, and differential testing covers only the inputs someone thought to try. So every accepted statement is also executed against real Python, a step that caught several proofs which were logically valid yet still wrong about the implementation's real behavior.

Why it matters

Python has no precise written definition; in practice the language is whatever CPython does, and the reference manual says little about the odd corners where bugs live, such as an object mutating a dictionary mid-lookup or a value sitting one past what the C code was written for. Forcing exact, total statements about behavior is a way to expose where code fails to do what everyone assumes. This project suggests that AI labor combined with mechanical checking can bring formal verification to a large, decades-old C codebase, provided the meaningless-proof problem is engineered away through adversarial review and differential testing. The concrete yield is 418 real defect reports, dozens of them capable of crashing the interpreter or corrupting memory.