Using Lean to Improve Python

I had Opus 5.5 formalize CPython in Lean: 613,318 lines of Lean that copy Python's internals line by line, tested against the real interpreter and checked by Lean.

On the way it found real bugs in Python, including crashes from plain Python code. 🧵

How it works: for each function in CPython 3.15.2, an agent writes a Lean model that mirrors the C or Python source. The model runs against python3 on 50,000+ generated inputs until they agree. Then it proves properties about it, and a second agent reviews every function.

One of the bugs: five lines of plain Python that segfault Python 3.15.

Instances of a class share one table of attribute names. dict.setdefault on an instance's __dict__ misses the case "this name exists, but not on this object", and dereferences a null pointer.

The hard part wasn't the proofs. It was proofs that prove nothing: a theorem Lean accepts can still say nothing true about Python. Independent review threw out more than half of the early work, so only functions that pass review count: 4,071 so far.

So far: 4,071 functions reviewed, 3,834 properties proved, 588 refuted, 418 bug reports with reproducers. We've started reporting them to CPython, beginning with six crashes, each reproduced on 3.15 and main.

Write-up: broyojo.com/python-formali…
Code and every bug report: github.com/Broyojo/python…

Most of CPython is still unexplored, and contributions are welcome. The same method should work for other languages and libraries too; the write-up explains how.