I used agents to find 25 bugs in free-threaded CPython

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

Claude Opus 5.5 agents confirmed 25 bugs in CPython's build without the Global Interpreter Lock, each on an unmodified interpreter. A tracker search found no earlier report for 18 of them. A later sweep of 1,805 call sites confirmed 92 more findings. Two independent provers also proved the locking model's safety invariant. Checking that proof against real runs showed five places where CPython doesn't behave like the 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.

I tested free-threaded debug builds of main (6757482), 3.15.0rc2+ (2dafe2a) and 3.14 (1d8c9f8). I also used release and ThreadSanitizer builds of main, and a python.org 3.14 GIL build for comparison. Claude Code directed every agent, all of them Claude Opus 5.5. 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. No agent filed, commented or posted anything.
• Every run has a hard timeout, and patches go into isolated copies of the source.

The bugs

The hunt ran in three rounds: 221 agents, about 22 million tokens, about 13 hours. One agent owned each subsystem. Later stages reproduced, attacked, fixed and reviewed what it found. A critic ended each round and listed the gaps for the next one.

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 an outside reviewer pushed on novelty, a second systematic search of the tracker found no earlier report for 18 of the 25. Three of those have no related report at all. The other 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. The packets need another round of fixes before filing. Eight have blocking errors, including a fix that must be restructured to link on 3.14 and Windows, and several wrong repros or claims. Four of the 25 are filed so far, 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 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 auditors found, not from the 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 three independent checks. 92 are confirmed, 8 are duplicates and 1 was refuted.

So these are not 92 free-threading bugs. 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 checkers' notes. A shortlist of 10 is ranked for filing. It has not had a maintainer-style review yet.

What the spec did

Midway through, I tried letting the formal side lead. Agents wrote the locking protocol down before looking for bugs. The spec says how critical sections, pinning and stop-the-world pauses are supposed to interact, in 698 lines of TLA+ with 13 contracts and 12 rules for callers. Then they checked code against it.

• Blind recall. Checked against six known bugs 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.
• New bugs. Checking call sites against the rules found three. The best is a use-after-free that aborts debug builds on main, 3.15 and 3.14. ThreadSanitizer flags it as a data race on freed and reused memory. It has a one-hunk fix and a stress test that fails 5 of 5 runs before it, and it is filed as gh-158198. 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, 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 and no native_decide.

Are the proofs real?

Agents are good at making a proof look finished, so an audit tried to catch the proofs cheating or proving nothing:

A broken spec here has one deliberate defect, such as a deleted guard or a lock left held. The model checker first confirmed that each defect 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 trace 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. None has been re-proved yet.

So the proof holds, but it is about a cleaner protocol than the one CPython runs. The audit found five of the 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 independent checks on every candidate.

Interpretation and limits

Agents with a strict repro harness found real, mostly new bugs in mature, heavily reviewed code. 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 the modelled protocol, at its default settings, meets its 11 safety properties. Checking them against real runs showed where CPython's actual protocol differs.

• "No earlier report found" means a systematic search came up empty, not that no one has ever seen the bug.
• Six of the 25 have no packet yet, and 8 packets have blocking errors to fix before filing.
• The proofs cover safety only. One of the 16 theorems is established by neither prover: that a reduced core of the invariant, without its three extra conjuncts, is inductive by itself.
• 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.
• 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

• File the remaining packets upstream and link them here.
• 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