AI agents rewrote CPython in Lean and uncovered 418 Python bugs
Formalizing CPython
Opus 5.5 agents copied CPython's functions line by line into Lean, tested each copy against real Python on tens of thousands of inputs, and proved properties that a second, independent agent had to verify. The result: 613,318 lines of Lean across 1,539 files, 18,898 theorems, and 4,071 accepted functions. Along the way the proofs exposed 418 bug reports, about 55 of them capable of crashing the interpreter or corrupting memory from ordinary Python code.
The hardest part wasn't getting AI agents to write proofs. It was getting proofs that actually mean something.
- debugnik
Wouldn't it be more productive spending the tokens on adding ACSL annotations to verify CPython with Frama-C? You'd verify the actual runtime instead of an AI translation of it, and fixes could be contributed upstream directly.
- anewhnaccount2
Same approach for Julias stdlib: https://discourse.julialang.org/t/formalizing-julia-in-lean-...
- jakobnissen
I think this approach to bug hunting is super promising (obviously - it finds a ton of bugs). The long-term problem is how this kind of bug-hunting can be done routinely, e.g. as part of a test suite. The approach taken by these people, the same approach as when the Julia folks did it, isn't really automatable, because it requires a lot of both human and AI agent work.
I guess longer term it needs to be built into the language, to prevent code and lean proofs from drifting. I.e. it could be opt-in properties that are written along the code, and which is then checked in the test suite. So very similar to ordinary compiler checks, except more expressive and expensive, and done only at test time.
- tomtom1337
I'm confused about a few points, would love it if someone could help clear it up!
- if the rewrite in Lean happens line-by-line, how can the two implementations differ in their result (Step 2)?
- how does this approach know "something that should always be true" in Step 3 (is it the intelligence of the LLM "guessing"?).
- erfgh
Does anyone read articles written by AI? This is a serious question.