Five Lines of Python That Crash 3.15

Five lines of ordinary Python are enough to crash the current 3.15 interpreter, and it was an AI that found them. It turned them up while doing formal verification, the slow, expensive, machine-checked kind of correctness work usually left to specialists. Two Georgia Tech researchers had Claude Opus 5.5 rebuild CPython’s internals in Lean, a language where every proof is checked by a computer, and real Python bugs fell out along the way.

Here is the crash. No threads, no C extensions, no callbacks that reach into memory. Just two objects of the same class, one missing attribute, and a call to dict.setdefault.

from enum import StrEnum

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 fault

Instances of a class share one table of attribute names. setdefault on an instance’s __dict__ misses the case where that name exists on the shared table, but not on this object, and then dereferences a null pointer. David Andrews reported the crash as CPython issue 161693. It reproduces on Python 3.15.2 and on the development branch, with no special setup. A fix, pull request 161704, has been approved by core developer Inada Naoki and is waiting to be merged. The same reviewer also labeled it for backport to 3.15 and 3.14.

The crash is real. The method behind it, an AI agent doing formal verification at scale, is the bigger story, and also the easier one to oversell.

A line-by-line copy, in eleven days

Andrews is a computer science Ph.D. student at Georgia Tech, advised by Chao Zhang. Starting on October 29, 2026, they had Claude Opus 5.5 write a Lean 4 model of CPython 3.15.2 that follows the C and Python source line by line. Eleven days later, on November 9, they posted the results and opened the repository. The work ran on two Claude Ultra accounts. Andrews said he stopped early, after about $6,978 of API-equivalent usage, because a day of work used a week’s allowance.

Each function went through the same four steps. An agent rewrote it in Lean, including error messages and odd corners, with citations back to the 3.15.2 source. The copy was run against the real interpreter on at least 50,000 generated inputs. Then the agent tried to prove a property about all inputs, or to prove the property false and keep the counterexample. A second agent, which had not written the model, reviewed the work against the original source, reran each property on real Python, and asked whether a broken implementation would also satisfy the theorem. Only the functions that survived that review are counted.

The published snapshot is 613,318 lines of Lean in 1,539 files, with 18,898 theorems and lemmas. I counted the Lean files in the project’s PyLean tree and got the same line and file totals. 4,071 of the 26,004 functions in scope have passed review, or 15.7%. Coverage is uneven. The grammar rules are done. The standard library, which is large and mostly written in Python, is at 9%, and the interpreter core is at 10%.

This is a mirror of CPython’s actual source, not a formal semantics of the Python language, and not a proof that the Lean is equivalent to the C. The example the authors lead with is the function that counts how many numbers are in a range:

The Lean copy keeps C’s unsigned wraparound past 2⁶⁴. The accompanying proof is meant to show that this function, the slower path for very large numbers, and the code that chooses between them always give the same count.

Proofs that prove nothing

A checked proof guarantees that a statement follows from the Lean copy. It does not guarantee that the copy matches real Python. The authors are clear about this, and it is the most important caveat in the work.

The hardest part wasn’t getting AI agents to write proofs. It was getting proofs that actually mean something.

David Andrews and Chao Zhang

Their first pass asked for breadth: copy every function and prove at least one thing about it. The agents did. A later review threw out more than half of that early work. In one file, only 21% held up. The proofs were formally correct. They just didn’t say anything useful. “If this function returns a number, the number is at least zero” is also true of a function that always crashes. The reviewer now asks a simpler question: could a broken version of the function pass this proof too?

Tests against real Python also caught proofs that were valid in Lean and still wrong about CPython. A JSON encoder “proof” assumed allocations always succeed, including a 16-terabyte indent string. A pickle nesting-depth proof missed a codec that loads only in a fresh process. A model of set assumed that freed memory addresses never come back, which hid a real memory bug once allocator reuse was modeled.

418 reports, six bugs filed

When a proof failed because Python itself was wrong, not the copy, they wrote it up. The repository holds 418 reports that still reproduce on 3.15.2, each with a short script. That is not 418 confirmed CPython bugs, and it is not 418 filings. The project’s own findings file opens with the line, “Nothing here has been filed.”

The authors group about 55 of the 418 as serious enough to crash the interpreter or corrupt memory from ordinary Python code, usually by having user code change a container in the middle of an operation. Python does not treat running hostile Python code as a security boundary, so they frame these as ordinary bugs, not security issues. Most of the rest are smaller: a wrong error message, a disagreement with the docs, or a C implementation that disagrees with its pure-Python twin. 129 of the 418 are of that last kind.

Six crashes were filed with CPython on November 9, shortly before the public post. Andrews says he read and reproduced each of them himself. All six were still open on November 10. None has been closed or formally marked confirmed as an issue state. The strongest signals so far are labels, an assignment, and third-party fix requests.

What the critics got right

The announcement made the rounds quickly. The original thread had about 88,000 views by the morning of November 10. A Hacker News discussion had 79 points and 31 comments as of that afternoon. An announcement on the Python core development forum still had no replies. Core-developer reaction, where it exists, is on the GitHub issues and pull requests, not on the forum thread.

The most serious objections are about what the word “formalize” is being asked to do. The proofs are about a Lean translation written by an AI model, checked on a finite set of tests, and then accepted or rejected by a second AI reviewer. That process can find real bugs, as the setdefault crash shows. It does not show that the proofs all hold for CPython itself. Other commenters asked why not annotate the real C and check it with a tool such as Frama-C, rather than trust an AI translation. Andrews’s answer is that about half of CPython is written in Python, where Frama-C would not help, and that CPython’s C is dynamic enough that such a tool could lose precision. He also said, more simply, that he does Lean for fun.

Those limits are real. A line-by-line copy can inherit the original’s bugs, or introduce new ones that tests miss. Absence of a report is not evidence that the unmodeled 84% of CPython is fine. Multithreading is out of scope, and the project ran out of quota before it finished.

This happened first in Julia

The method is not unique to Python. The authors say they were following Miles Cranmer’s julia-in-lean project. On October 25, two weeks earlier, Cranmer reported about 400 candidate bugs in Julia’s Base library, of which he had filed 75 after manual filtering, at a cost of about $5,000 in API-equivalent usage. A lesson from that work shaped the CPython review rule: when proving that unsafe index operations stayed in bounds, 128 of 130 “proven” sites had just assumed the index was in bounds.

By November 10, Cranmer’s repository totals had already moved on, to 689 bug write-ups and 107 issues filed. The useful comparison is the earlier snapshot, taken when the method first became public.

A useful way to find bugs, not a verified Python

What stands up is narrower than the headline “we formalized CPython,” and still worth taking seriously. In eleven days, an AI-written, machine-checked model of part of the interpreter turned up a handful of real crashes, including one that takes five lines of ordinary Python. A core developer has already approved a fix for that crash. The same process also produced hundreds of reports that have not been filed, and thousands of early proofs that had to be thrown out because they didn’t prove anything that mattered.

Python still has no precise written definition. In practice, “Python” means whatever CPython does. A Lean copy of the source, tested against the real interpreter, is a way to press on the odd corners of that de facto specification. It is not a proof that CPython is correct, and it should not be sold as one. Used carefully, with a human reading the filings and a reviewer who asks whether a broken function could also pass, it is a surprisingly effective way to find the five lines that should never have become a crash.