AI-Generated Lean Proofs Uncover 418 Bugs in CPython

By tasking AI agents with rewriting CPython's internal C code into Lean—a language designed for machine-checked mathematical proofs—researchers have uncovered 418 bugs in the Python interpreter. This formalization process, which has already produced over 600,000 lines of verified code, identifies critical issues that traditional testing might overlook by forcing a precise mathematical definition of how Python behaves in 'odd' edge cases.

This chart visualizes the scope and progress of the project's formalization efforts across the CPython codebase.

The Formalization Pipeline

The project follows a rigorous four-step pipeline to ensure the Lean model accurately reflects the CPython source. First, AI agents rewrite C functions into Lean, preserving exact logic including error messages and integer overflows. Second, these copies are run side-by-side with the real Python interpreter on at least 50,000 inputs to ensure they agree.

This image illustrates the first step of the pipeline where AI agents rewrite C code into Lean while preserving exact logic.

Chart drawn by HN Digest from figures reported by broyojo.com; values are shown as written in the source.

Third, the team states properties that should always be true and uses Lean's proof checker to verify them. Finally, a second AI agent that did not write the original model reviews the work to ensure it is 'faithful' to the source. Only functions that survive this independent review are counted as accepted.

“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.”

— Formalizing CPython

Identifying Hidden Bugs

Because a formal proof requires a precise definition of every possible state, the process revealed bugs where CPython's behavior deviated from its intended logic. For example, the team found a dictionary call that causes a segmentation fault when a specific key is used on an object's attribute dictionary.

Other findings include memory corruption in XML edits and a base32 decoder that produces incorrect padding depending on the position of ignored characters. The project also identified a discrepancy between the C and pure-Python versions of the pickle module, which give up at different nesting depths.

The Challenge of 'Useful' Proofs

A significant hurdle was preventing the AI from generating 'hollow' proofs—statements that are technically true but fail to catch broken code. For instance, a proof stating 'if the function returns, the result is at least zero' is technically correct even if the function always crashes.

This visual explains the concept of 'hollow' proofs where a statement is technically correct but fails to identify functional bugs.

To solve this, the reviewers now ask a specific question: 'could a broken version of the function pass it too?' If a broken version passes, the proof is rejected. This forces the model to be more realistic, such as accounting for memory requests that might fail or user code that throws errors mid-operation.

Limitations and Trade-offs

While formal verification provides high confidence, it is currently limited to a small fraction of the codebase. The project has covered about 15.7% of the functions in scope, as modeling every complex edge case in a massive, old codebase like CPython is labor-intensive.

Furthermore, a checked proof only guarantees that a statement follows from the Lean model, not necessarily the real Python interpreter. If the model itself is incomplete—such as assuming memory requests always succeed when they might not—the proof can remain valid while the real software remains buggy.