A TLA+ Playbook for Your Scheduler, Queue or Retry Loop

Boris Cherny posted that two prompts and a Lean model of the Claude Agent SDK produced 16 PRs fixing races. The recipe: model the race-prone part, find counterexamples, reproduce, fix.

We ran it on Agent Swarm with TLA+. One day, ten bugs, all fixed on main. Five steps, one prompt each. Paste, rename, run.

The one rule: TLC checks the model, never your code. Every spec action maps to a line, and a counterexample only counts once a test reproduces it.

Step 1: pick the target

Rank subsystems by concurrency risk and bug history. Pick one with a transaction boundary, several writers, and two fixed bugs to calibrate on. We took the workflow engine and the heartbeat, one agent each.

Rank the 3 to 5 subsystems in this repo with the most concurrency risk.
Use file paths, git log and merged PRs mentioning race, duplicate,
stuck, re-fire.
For each: the files, the actors that write the same rows, candidate
invariants, the fixed bugs a model should rediscover.
Recommend one first target. No spec yet.

Step 2: model it, then calibrate on fixed bugs

Write the spec and the action map together: each action, the file and line it models, the SQL guard it encodes. One transaction is one action. Every await outside one is where other actors interleave. Keep constants small.

Then remove the guard a fixed bug added. The model must find that bug, or the model is wrong. Ours went 7 of 7, and found the first new bug on the way: a later commit had swapped an original fix for a weaker gate.

Model <subsystem> in TLA+ under specs/tla/<subsystem>/:
- <Subsystem>.tla: state, Init, one action per code path that reads or
  writes that state. Small constants: 2 workers, 1 retry.
- <Subsystem>.cfg: constants, invariants, temporal properties.
- ACTIONS.md: every action, the file:line it models, the WHERE clause
  it encodes.
One DB transaction is one action; every await outside one is a boundary.
Actors: <pollers, sweeps, user cancel, crash, restart>.

Then calibrate on <fixed PR list>: add a constant that removes each
fix's guard, run TLC with it off, record the violated property and
state count in CALIBRATION.md, keep a control config with it on. If a
known bug is not found, fix the model. Do not fix any code yet.

Step 3: every counterexample becomes a failing test

A trace is a suspect, not a bug. Map each step through the action map and write a test that calls the production functions in that order. It must fail on main. If it passes, the model drifted: fix the spec.

Seven workflow traces, seven failing tests, zero drift, four root causes. Three more from the heartbeat.

Run TLC on the current guards. For each counterexample:
1. Map every trace step to code through ACTIONS.md. No row: fix the
   model first.
2. Write a test that calls the production functions in trace order on
   a temporary database. Hold mid-flight executors on a barrier.
3. It must fail on main. If it passes, log model drift, fix the spec.
4. Commit it as expected-to-fail.

Step 4: fix, one PR per root cause

Flip the repro to a plain test. Add a fix flag to the spec, a control config that still finds the old bug, a fix config that holds.

When the model shows the design is the problem, let it design the replacement. Our old heartbeat was a chain of sweeps. The new one is two actions, checked before a line was written, in review as #1682.

Fix <CX list>. One PR per root cause.
1. Fix the code. Flip the repro from expected-to-fail to a plain test.
2. Add a Fix flag to the .tla that keeps the pre-fix branch, plus
   Ctl-<CX>.cfg (flag off, still finds the bug) and Fix-<CX>.cfg
   (flag on, holds). Rerun TLC, report the counts.
3. PR body: what the model found, the trace, the counts.
Open the PRs. Do not merge.

Step 5: keep the spec true, in a swarm

A spec rots the day a mapped file changes. So a daily workflow lists PRs merged since the last watermark, fans out one agent per touched spec, reruns TLC, reduces into one PR, polls CI, merges, notifies. A drift gate catches silent failures. Every node below is real.

First scheduled run, this morning: six merged PRs touched mapped files, both specs updated, one PR merged in 22 minutes, nobody in the loop.

Set up a daily job that keeps specs/tla/ true to the code:
1. Plan: PRs merged since the last watermark, per spec, that touch a
   file named in its ACTIONS.md.
2. Map: one agent per touched spec. Re-check the changed rows, update
   the spec, rerun control and fix configs, push a branch or no_change.
3. Reduce: one PR with every changed spec and the PRs that caused it.
4. Gate: poll CI, merge only if the PR touches specs/tla/ alone. Notify
   on merge or failure. Alert if plan or reduce failed silently.
Advance the watermark only after the PR merges.

What we got

Main, 2026-09-29:

• 3 specs, 1,415 lines of TLA+. 7 of 7 known bugs rediscovered.
• 10 new bugs: 7 workflow traces (4 root causes) and 3 in the heartbeat. 8 repro tests on main, all green.
• 7 fix PRs merged 2026-09-28, same day as the models.
• Largest counterexample: 338,137 distinct states. Largest clean run: 928,920.
• New heartbeat: 8 properties, 4,243 states, under 2 seconds. Review still caught a fence keyed on the wrong field, which the model never saw.
• 3 more traces (CX8 to CX10) have no repro yet and do not count.

Reproduce it

TLC is Java 21 plus tla2tools.jar; the rest is in specs/tla. This rediscovers a historical bug:

cd specs/tla/workflows && java -cp tla2tools.jar tlc2.TLC -workers auto -config Cal-bf12ab53.cfg Workflows.tla

Showreel music: "Mist City" by Section7, CC BY 4.0.