A TLA+ Playbook for Your Scheduler, Queue or Retry Loop
Five steps, one prompt each: model a concurrent subsystem in TLA+, calibrate it on bugs you already fixed, turn every counterexample into a failing test, and keep the spec true with a daily swarm workflow. Our run found ten reproduced counterexamples across seven root causes in a day.
A TLA+ model finds a race in a scheduler, queue or retry loop by making each database transaction one atomic action, and each await between transactions a point where other actors can run: pollers, sweeps, cancel, crash, restart. TLC explores every interleaving of those actions within small constants and reports a violated invariant as a step-by-step counterexample trace. The trace only counts once a production test reproduces it.
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 reproduced counterexamples across seven root causes. The dated results below distinguish traces, tests, and merged fixes. 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 heartbeat is a chain of sweeps. HeartbeatSimple.tla is the two-action replacement, checked before a line was written: model-checked, not implemented. The proposing PR, #1682, closed unmerged.
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 reproduced counterexamples: 7 workflow traces across 4 root causes, plus 3 heartbeat findings. 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 design: 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.
Since then, verified on main 2026-11-03: calibration is still 8 of 8 (workflows 2 of 2, heartbeat 6 of 6); specs total 2,020 lines (Heartbeat 578, HeartbeatSimple 264, Workflows 1,178). CX11 stays fixed by #1832, and #2377 closed CX13, the finalizer that completed a cancelled run. Six traces have no repro test yet: CX8 to CX10, CX12, CX14, and CX15, found by #2364. The heartbeat replacement never left the model: HeartbeatSimple.tla is the two-action design, 8 properties, 4,243 states, under 2 s, model-checked, not implemented. The proposing PR, #1682, closed unmerged.
Symptom to invariant
| Race symptom | Modeled state | Invariant violated | Counterexample shape | Production test | What TLA+ cannot prove |
|---|---|---|---|---|---|
| Two workers run one task | Task status, agentId, claim reads |
OneRunner (C1) |
ClaimRead(w1) → AutoAssign(w2) → PollStart(w2) → ClaimWrite(w1) |
budget-claim-gate.test.ts, "two-agent race: only one task is claimed; the other gets task_assigned for a different task or null" |
Code drift from ACTIONS.md: TLC keeps checking the modeled guard. |
| Heartbeat overwrites a task the worker just completed | Stall snapshot (HbRead), task status |
TerminalAbsorbing (C2) |
AutoAssign → PollStart → Age → HbRead → Complete → HbWrite |
task-supersede-resume.test.ts, "supersede on already completed task returns null" |
Timing beyond the modeled constants: Age is an abstract stall threshold. |
| Progress write overwritten by a stall supersede | lastUpdatedAt, modeled as the counter ver |
NoLiveKill (C3) |
AutoAssign → PollStart → Age → HbRead → Progress → HbWrite |
heartbeat-stall-cas.test.ts, "stall classifier does not supersede a task that made progress after the candidate read" |
Fields the model does not track: the review-caught fence keyed on the wrong field. |
| Join fires while a branch waits for its retry | completedNodeIds, retry-pending row |
JoinWaitsForBranches (CX8) |
26-state trace: the join runs without the retrying branch | None yet (open) | Code that splits a mapped transaction into two awaits. |
| Finalizer completes a cancelled run | Run status | TerminalRunStaysQuiet (CX13) |
XCkWait (B waiting) → TaskFinish(B ok) → E1 → E2 (run running) → Cancel → EFin (run completed) |
workflow-cascade-cancel.test.ts, "callbacks that read the step before the cancel commit route nothing after it" |
The child-run tree: the model is one run, so the code that cancels a run's children, and refuses their late work, is never checked. |
Questions
Does TLC check my model or my code?
The model only. ACTIONS.md maps each action to a file and line, and the daily sync re-checks a row when its file changes.
Race or deadlock: which does it find?
Both. Safety invariants catch races, such as two runners on one task (OneRunner) or an overwritten terminal state (TerminalAbsorbing); liveness and temporal properties catch stuck states (SupersededGetsResume, EventuallyFinished).
What happens after a counterexample?
Map every trace step through ACTIONS.md; no row for a step means model drift: fix the spec first. Then write a test that must fail on main, fix one root cause per PR, and add control and fix configs.
Reproduce it
TLC is Java 21 plus tla2tools.jar; the rest is in specs/tla. This rediscovers a historical bug:
TLA2TOOLS_JAR=/absolute/path/to/tla2tools.jar
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.
Related field notes
We Rebuilt Linear's “Loops updates” Clip as a Swarm Video in Eight Rounds
Three video models read Linear's motion-design teaser; the two Gemini models called the 3D scene 2D until 7.5s. A frame-by-frame check caught it. The replica is 858 frames of Remotion and three.js, reviewed eight times.
TasteLabs Found Design Drift in Our Own Sites
Our landing sites had three amber ramps, 34 untokenized brand-color literals, and no BRAND.md files. One fix PR has merged; one is still open.
Right-sizing Your Agent Swarm: What Container CPU and RAM Graphs Are Really Telling You
A straight-line CPU climb and a coder worker stuck near 1.1 GB looked like production problems. They were metric interpretation traps. Here are the sizing numbers we actually run.