25 bugs in free-threaded CPython, found by agents

[ 2026-09-25 · updated 2026-10-23 ] // Claude Opus 5.5 · TLA+ · Lean 4 // 14 MIN READ

Claude Opus 5.5 agents confirmed 25 bugs in the free-threaded build of CPython, the build without the Global Interpreter Lock. Each has a trigger that misbehaves on an unmodified interpreter, and 18 have no earlier report found in the tracker search. I filed five reports upstream, and CPython developers have since merged fixes for two of them. Proofs in TLAPS and Lean checked a model of the locking protocol; replays of real runs showed five places where CPython departs from that model.

Setup

PEP 703 made CPython's Global Interpreter Lock optional. 3.14 is the first release where the free-threaded build is officially supported. Removing the lock took new machinery. Per-object locks called critical sections are quietly released when their thread blocks. Stop-the-world pauses park every other thread. Dicts and lists get lock-free reads. Bugs tend to live where two of these meet, or in older code that assumed nothing else could run while it did. When this machinery is wrong, ordinary threaded Python code can crash, corrupt memory or hang the whole interpreter. I started with one question: could agents working with formal tools, the Lean proof assistant and the TLA+ specification language, find real bugs in mature code? This machinery seemed a likely place to look.

I tested free-threaded debug builds of main (6757482), 3.15.0rc2+ (2dafe2a) and 3.14 (1d8c9f8). I also used release builds and ThreadSanitizer (race detector) builds of main, and a python.org 3.14 GIL build for comparison. Every agent was Claude Opus 5.5, directed from Claude Code. They worked inside a harness: the workflow that gave them builds and tools, ran their triggers, sent each finding to separate checking agents and kept the evidence. The ground rules:

• A bug counts only if a trigger misbehaves on an unmodified build. A model or a code reading alone is never enough.
• Findings are checked by separate agents: one writes its own repro from the description, one tries to refute the finding, and one searches the tracker for earlier reports.
• GitHub is read-only during the hunt: no hunt agent filed, commented or posted anything.
• Every run has a hard timeout, and patches go into isolated copies of the source.

I chose the target and these ground rules, steered a lead agent, decided which findings to report and filed the reports from my GitHub account. The lead agent scripted each round, re-ran key repros and chose what went into the next round; the other agents read the C code, wrote the triggers, repros, patches, specs and proofs, and drafted the reports. Separate agents, not people, did the three checks above, and checks by CPython developers began after filing.

The bugs

The hunt ran in three rounds. One agent owned each subsystem; later agent stages reproduced, attacked, fixed and reviewed what it found, and a critic agent ended each round by listing the gaps for the next.

It ended with 25 bugs: 16 I'd file now and 9 at low priority. They include whole-interpreter deadlocks, heap corruption, NULL dereferences in lock-free iteration and use-after-frees. Most affect the 3.14 branch as well as 3.15 and main. Eight also hit the regular GIL build. Most need only public Python APIs to trigger. A few need a private module, API misuse or a C-API callback.

After a review questioned the novelty claims, agents searched the tracker again, systematically. For 18 of the 25 there was no earlier report found in the tracker search: three have no related report at all, and 15 have related work on the same components only. Six others partly overlap an earlier report. One was already described upstream but is still unfixed.

19 of the 25 have a filing packet: a minimal repro, fix diffs for each branch, a regression test that fails before the fix and passes after, and a model check of the fix. Eight of those packets have blocking errors, including a fix that must be restructured to link on 3.14 and Windows, and several wrong repros or claims, so they are not filed yet. Four of the 25 are filed, all from packets without blocking errors: two deadlocks in type locking (gh-158194, gh-158195), a heap double free in FileIO (gh-158196) and a NULL dereference in instance-dict iteration (gh-158197). A fifth report, gh-158198, comes from the spec pilot below. The other 21 bugs are described here by class and count only, with no function names, triggers or repros until they are reported.

A second pass: the call-site sweep

Writing the spec (below) surfaced five rules for code that calls these primitives. Two of them: "don't use a borrowed pointer after anything that can run Python" and "don't act on an unlocked read". The rules came from gaps that auditing agents found, not from the locking model itself. Agents then checked 1,805 call sites in 114 files against them. 252 candidates merged into 101 findings, and every finding got the same three separate-agent checks. 92 are confirmed, 8 are duplicates and 1 was refuted.

So these are not 92 free-threading bugs, and they are not part of the 25. About half are general CPython bugs that the rules happened to lead to. The 11 same-object races are a class upstream has closed as "not planned" before. The build-scope split is a heuristic from the checking agents' notes. One agent ranked a shortlist of 10 for filing; those still need packets and the agent review the hunt's bugs got.

What happened upstream

I filed the five reports on 25 and 26 September 2026, each with a repro and a proposed patch.

The two merges are the strongest outside check on this work so far. In both, a CPython developer wrote or refined the final fix and other developers reviewed it, so neither is an agent patch merged unchanged. For gh-158198, my patch made freeing the object take the dict's lock; DinoV's change instead clears the dict's pointer to the object's inline values only after they have been moved out, and reads it with acquire ordering when the object is cleared.

Merged does not mean released on every branch. The gh-158197 fix is listed in the Python 3.15.1 changelog; its PR is labelled for a 3.14 backport, but none has been opened. The gh-158198 fix is in main only.

What the spec did

Midway through, I tried letting the formal side lead. Agents wrote the locking protocol down before looking for bugs, in TLA+, a language for describing concurrent systems precisely enough for tools to check them. The spec says how critical sections, pinning (keeping a lock held even while its thread waits) and stop-the-world pauses are supposed to interact, in 698 lines with 13 contracts and 12 rules for callers. Then agents checked code against it.

• Blind recall. Checked against six bugs from the hunt that it had never been told about, the pilot rediscovered five.
• One confirmed prediction. The model predicted a path into a stop-the-world deadlock. An instrumented build then hung 5 times out of 5. It is a new entry point into an already-known deadlock, not a new bug.
• A named root cause. The spec had to state an assumption the code never documents, and deadlock freedom depends on it. Audits of the code and replays of real runs showed that shipping CPython breaks it. It is the root of that deadlock family.
• Three more bugs, separate from the 25 and the sweep, found by checking call sites against the rules. The best is a use-after-free that aborts debug builds on main, 3.15 and 3.14, which ThreadSanitizer flags as a data race on freed and reused memory. I reported it as gh-158198 with a one-hunk patch and a stress test that fails 5 of 5 runs before the patch; the merged fix is DinoV's own. The second is a free-threaded hang. The third turned out to be a GIL-build bug.

The proof held; the model didn't match CPython

Next I asked for real proofs, not bounded checks. The spec's safety invariant has 24 parts and implies 11 safety properties, such as "no lock is leaked". It was proved twice, for any number of threads and any nesting depth:

• TLAPS, the TLA+ proof system, by a lead agent and five helpers: 4,430 of 4,430 proof obligations, and 4,455 of 4,455 for a version with any number of locks.
• Lean 4, a proof assistant whose small kernel checks every step, by one agent that wrote a fresh encoding of about 5,000 lines without reading the TLAPS proof. It uses only Lean's three standard axioms, with no sorry (a placeholder for a missing proof) and no native_decide (which trusts compiled code).

Both are proofs about the modelled protocol, as written in the TLA+ spec and re-encoded in Lean, not about CPython's C code.

Are the proofs real?

Agents are good at making a proof look finished, so separate agents audited the proofs, trying to catch them cheating or proving nothing:

A broken spec here has one deliberate defect, such as a deleted guard or a lock left held, which the model checker first confirmed actually matters. A proof that still passed on one would be proving nothing, and none did. Some of those failures are shallow: the proof just restates a setting that was changed. The any-number-of-locks version was not mutation-tested. So the answer is yes: within the model, these are real proofs.

They are safety proofs only. Deadlock freedom is not just unproved: under CPython's documented settings it fails in the model, with a 13-state trace that is the deadlock path the spec predicted and a real build then hit.

Is the model CPython?

A proof is only as useful as its model, so the last step checked the model against the real interpreter. First, the audit added one behaviour the spec had left out: a thread woken from a wait re-attaches before it retries the lock. With that added, the proved invariant becomes false after four steps. The 11 safety properties themselves still held in every bounded check, up to 23.5 million states with three threads.

Then a checker replayed recorded runs of an instrumented build: 36.1 million events from 44 logs. It evaluated the invariant on every state it reconstructed. The original invariant failed at every stop-the-world wake-up it tallied, as the audit predicted. Ordinary lock-wait wake-ups did not break it. The checker also found four more places where CPython does something the model forbids:

• a critical section taken on the fast path inside a stop-the-world pause;
• critical sections inside global pauses;
• brief, uncontended raw holds of the type lock;
• the world restarted before the pause's own lock is released.

On the states the checker classed as ordinary, all 10 safety properties it could evaluate held. That class excludes global pauses, forked children, finalization and the raw type-lock holds. The one property that failed anywhere was the no-leaked-lock rule, on those raw holds. Each gap has a proposed spec fix that passes bounded checks but has not been re-proved.

So the proof holds, but it is about a cleaner protocol than the one CPython runs. The audit and the replays found five places where the two differ. Without the check against real runs, the proof would have been a correct theorem about the wrong system.

Did the rules help find bugs? A control run

I re-audited 8 of the sweep's areas with a plain "find free-threading bugs" prompt. The model, tools and builds were the same, and the agents were told not to read the earlier work.

The rules reached a subtle class the plain prompt missed: five re-entrancy chains. Their output was also cleaner, but it had been through more checking. They did not find more bugs overall. What I'd recommend is a plain audit for breadth, then the rules as a checklist, with the three separate-agent checks on every candidate.

Interpretation and limits

Agents with a strict repro harness found real bugs in mature, heavily reviewed code, most with no earlier report found in the tracker search, and CPython developers have merged fixes for two of the five I reported. The TLA+ spec made one prediction that came true, named a root cause and produced a checklist. The unbounded proofs found no bugs. They showed that the modelled protocol, at its default settings, meets its 11 safety properties, and checking them against real runs showed where CPython's actual protocol differs.

• I have not reported the other 21 hunt bugs, the other two pilot bugs or the 92 sweep findings, so apart from the one hunt bug already described upstream, they have had no upstream review.
• One of the 16 theorems is established by neither prover: that a reduced core of the invariant, without its three auxiliary parts, is inductive on its own, meaning every step preserves it without relying on those parts.
• The replays cover 44 of 72 logs and 16 of 38 workloads, with no data writes, so one property went unchecked. Some known kinds of divergence never occurred in them, so there may be more gaps than the five found.
• The models assume sequential consistency, a single global order for all memory operations, which arm64 hardware does not guarantee, so they cannot show memory-ordering bugs.
• The control used 8 areas, and the same model helped write the rules, so rule-style thinking may have leaked into the plain run.
• Everything ran on one macOS arm64 machine. Linux, Windows and 3.13 are untested.

Next experiment

• Fix the eight blocked packets and file the remaining reports, so more of the 25 get upstream review.
• Check the roughly 9 candidates only the plain prompt found.
• Fold the five spec fixes into one model and re-prove it in both provers.
• Replay the remaining 28 logs, with data writes recorded.
• Repeat the hunt on Linux.

Reproducibility