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.
CPython · Objects/rangeobject.c
static unsigned longget_len_of_range(long lo, long hi, long step){ assert(step != 0); if (step > 0 && lo < hi) return 1UL + (hi - 1UL - lo) / step; else if (step < 0 && lo > hi) return 1UL + (lo - 1UL - hi) / (0UL - step); else return 0UL;}Lean copy · RangeSlice/Model.lean
def getLenOfRange (lo hi step : Int) : Int := if step > 0 ∧ lo < hi then uadd 1 (usub (usub (toU hi) 1) (toU lo) / toU step) else if step < 0 ∧ lo > hi then uadd 1 (usub (usub (toU lo) 1) (toU hi) / usub 0 (toU step)) else 0 -- step ≠ 0 is assumed by every proof-- uadd, usub: C's unsigned arithmetic,-- which wraps around past 2^64Checked and acceptedWritten, not yet acceptedNot started
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.
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.
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?
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.
Functions accepted
Objects/typeobject.c135 of 142 accepted · 5 reviewsObjects/genobject.c56 of 56 accepted · 5 reviewsObjects/setobject.c46 of 46 accepted · 7 reviewsModules/_json.c45 of 48 accepted · 5 reviewsLib/enum.py37 of 39 accepted · 9 reviewsLib/random.py37 of 38 accepted · 3 reviewsObjects/abstract.c41 of 43 accepted · 2 reviewsObjects/rangeobject.c33 of 33 accepted · 2 reviewsLib/pickletools.py31 of 33 accepted · 2 reviewsModules/binascii.c35 of 40 accepted · 2 reviews
Rounds of review →
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 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.
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.
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.
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.
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:
Crash
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 faultMemory corruption
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 goneWrong error
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: <a@[ x]>\n\nhi\n",
policy=policy.default)
msg["Message-ID"]
# UnboundLocalErrorSilently wrong result
New in Python 3.15, the base32 decoder can ignore chosen characters. If = is one of them, where it appears still changes the result.
a2b_base32(b"AAAAAAA", ignorechars=b"=")
# Error: Incorrect padding
a2b_base32(b"AAAA=AAA", ignorechars=b"=")
# b'\x00\x00\x00\x00'Missing error
Giving an enum value to a second member should raise an error. If the class's __repr__ is broken, the error is swallowed and the call quietly does nothing.
class W(Enum):
A = 1; B = 2
def __repr__(self): return 5
W.B._add_value_alias_(3)
W.A._add_value_alias_(3) # returns NoneC and Python disagree
Python has a C pickler and a pure-Python one. They give up at different nesting depths. This difference was first reported in 2008 and is still open.
v = []
for _ in range(400): v = [v]
pickle.dumps(v, 5) # works
pickle._dumps(v, 5) # RecursionErrorEvery report, with its script, is in the repository.
None of this is specific to Python. It works for anything with source code you can read and a working version you can run: another language, a library, a file format, a compiler. What made the difference for us:
The instructions our agents worked from are in the repository and meant to be reused: AGENTS.md for the agents doing the work, REVIEW_PROMPT.md for the reviewers, and the full list of functions with their status in coverage/methods.
The closest project is julia-in-lean, which did this for the Julia language and directly inspired this one1. It modelled Julia's standard library in Lean, tested the models against Julia, recorded about 400 bugs and filed 75. Its finding that 128 of 130 quick proofs had quietly assumed away the hard case shaped our review rules. A recent paper models NVIDIA's PTX GPU instruction set in Lean to prove GPU kernels correct2, building on earlier formal work on PTX's memory model3.
For Python specifically, λπ4 and a K framework semantics of Python 3.35 described the language mathematically; this project copies CPython's actual code instead. Similar efforts exist for JavaScript6,7 and WebAssembly8, and CompCert9 and seL410 remain the high bar for fully verified software. Comparing two implementations on the same inputs, the testing half of this project, goes back decades11,12.
The project started on 29 October 2026. 4,071 of the 26,004 functions worth checking (15.7%) have been copied, tested, proved and accepted by review. The Lean code is 613,318 lines in 1,539 files, containing 18,898 theorems and lemmas; 3,834 of the top-level properties are proved and 588 are proved false with a counterexample. Most of Python is still ahead, especially the large part of the standard library written in Python itself. Multithreading is out of scope for now. In these 57 files, every function copied so far has passed review. The 30 with the most accepted functions:
Python/bytecodes.c310Grammar/python.gram278Lib/collections/__init__.py184Lib/_pydecimal.py160Lib/_pydatetime.py150Modules/_struct.c122Objects/longobject.c119Objects/listobject.c114Objects/memoryobject.c107Objects/dictobject.c104Objects/bytesobject.c100Objects/exceptions.c97Objects/unicodeobject.c94Objects/bytearrayobject.c93Modules/arraymodule.c84Lib/_collections_abc.py81Modules/_operator.c73Modules/itertoolsmodule.c72Modules/_collectionsmodule.c64Python/codecs.c61Lib/operator.py59Lib/_pyio.py58Objects/typeobject.c57Lib/weakref.py54Objects/genobject.c46Lib/urllib/parse.py46Parser/action_helpers.c43Modules/_zoneinfo.c43Objects/floatobject.c38Objects/tupleobject.c37The project is open, and help is welcome. Most of CPython is still unmodelled: pick a file whose functions are still marked todo in coverage/methods, follow AGENTS.md, and send a pull request. Independent reviews of existing work count as much as new models. See CONTRIBUTING.md.
@misc{andrews2026formalizing,
author = {Andrews, David and Zhang, Chao},
title = {Formalizing {CPython}: A Lean Model of {CPython} 3.15.2},
year = {2026},
howpublished = {\url{https://broyojo.com/python-formalization/}},
note = {Code: \url{https://github.com/Broyojo/python-formalization}}
}