What TLA+ found in nfltr: designs checked before code, code checked against them

November 6, 2026

nfltr is a relay that machines dial out to, a stream multiplexer under it (link), and a hub that runs Claude Code agents on other machines (distributed Claude Code). The bugs that hurt there are silent: a write that reports success while its bytes never arrive, a session that never ends, a revoked key that keeps working, a result delivered twice or not at all. They pass unit tests and -race, and show up later as a truncated download or a test that fails once in fifty runs.

After the process post, a reader asked how we had found our relay bugs. Honestly: mostly after shipping, from soaks, flaky tests and other people's test suites. Since 2026-11-01 we have worked the other way round. Every protocol, concurrency, storage or cross-process state machine is first written as a TLA+ spec and checked with TLC, the TLA+ model checker, before its code is written; then the Go code records what it does, and those recordings are checked against the spec. This post reports what that found in five days, what it missed, and what it costs.

Contents: the method · an example · what it found · how it made nfltr more reliable · traces · what it missed · cost · rerun it · fit

The method

One rule, applied in all five repositories (link, the relay SDK, the relay core, the relay server and nfltr itself): a change to a state machine whose bugs would be silent starts as a spec. The spec is the design section of the change; code starts only after TLC passes. Each spec lives in its repository's spec/ directory with a README that maps every spec action to the Go functions it models.

• Invariants and liveness. What must always hold (no data after a FIN, a result delivered once) and what must eventually happen (a session ends once both sides end it). TLC explores every reachable state of a small configuration: two sides, a few sessions, one crash.
• Coverage. TLC runs with -coverage 1; an action the model never takes is a bug in the spec, not a pass.
• Witnesses. For each invariant, a property TLC must violate, to prove the situation it guards is reached. Without one, an invariant can hold because nothing interesting ever happens. This caught one of ours: link's crash configuration had never actually crashed.
• Mutants. Every bug we find, and every failure a design prevents, is kept as a mutant: the spec with the old behaviour switched back on. make spec-mutants fails unless TLC reports a violation for every one. A spec that cannot tell the old code from the fixed one proves nothing about the fix.
• Trace validation. A build tag makes the Go code write one NDJSON line per spec action at the moment the state changes; without the tag the recorder compiles to nothing. The repository's existing tests run with the tag, and TLC checks that each recorded run is a behaviour of the spec. Traces from several processes carry vector clocks and are merged by causal order, never by wall clock. A trace the spec rejects means the spec or the code is wrong, and someone decides which.
• Model-based replays. The reverse direction: TLC's random walks through the spec are replayed against the real code, comparing state after every step.
• Drift check. Each spec README lists the files it models. A commit that changes one of them without touching the spec, or without a Spec-Reviewed: line saying why the spec still holds, fails CI.

Specs are layered like the code. link's spec states what a layer above may assume of a session (ordered, credited, a clean end only once the peer read the FIN). The relay core models link only by that interface, and a refinement check ties the interface to link's full spec. The hub's spec states what it assumes of the relay in the same way.

An example: a write that raced its own FIN

The first spec was link's, as a pilot of about 90 minutes. link carries many sessions over one connection; a session can be half-closed (CloseWrite) while another goroutine is still in Write. The model separates the two steps the code takes: Write checks the session under a lock, may wait for credit or its turn to write, and only then buffers its frame. The fix is the check on both sides of the wait:

\* A side may send data only while its write side is open and it holds credit.
DataOK(p, s) == ~ss[p][s].wfin /\ cr[p][s].on /\ Answered(p, s)

SendCheck(p, s) ==                     \* Conn.sendData, before it may wait
    /\ pend[p][s] > 0 /\ wt[p][s] = "no"
    /\ Mutant = "write-race" \/ DataOK(p, s)
    /\ wt' = [wt EXCEPT ![p][s] = "data"]
    /\ UNCHANGED <<...>>

SendBuffer(p, s) ==                    \* after the wait: check again
    /\ wt[p][s] = "data"
    /\ Mutant \in {"write-race", "turns-no-recheck"} \/ DataOK(p, s)
    /\ Buffer(p, s)
    /\ wt' = [wt EXCEPT ![p][s] = "no"]
    /\ UNCHANGED <<...>>

With the mutant write-race (the shipped code: no check), TLC found a data frame sent after the session's FIN, a few states deep. The peer had already queued a clean end and dropped the data; the writer was told everything was sent. A later review found the second half: with only the first check (turns-no-recheck), a write parked behind another goroutine's turn still sent after the FIN.

What it found

Each repository's spec/README.md lists its findings, with severity, the test that failed before the fix and the mutant that keeps it fixed. The READMEs count differently (some number review findings separately), so the totals below are approximate and from our reading: about 40 findings in the relay core, about 55 shipped-code fixes in the relay server, and dozens in link, the relay SDK and the hub. Most were low severity. These are the silent ones:

Some of these were caught in design, before the code they would have broken existed:

• Per-call credit for agent-to-agent calls. Calls on one agent connection shared a receive loop, so one stalled caller delayed its siblings by up to 10 s. The spec's invariant NoHOL (no call waits on another) came first, for one direction, then both directions on the four shared connection queues, then several senders on one call; the code followed. The flaky test that had shown the stall reproduced it once in about 300 to 3,000 runs; the design removed the cause instead of widening its deadline.
• The orchestrator's task protocol. We wrote the protocol as it was (Orch.tla), let TLC find a turn run twice under one id in 10 states, wrote the design (OrchDesign.tla) and checked it, then deleted the code path that redispatched under the same id.
• Fixes that the checker refuted. The first proposed fix for a share-link expiry race, and a proposed "floor" rule for a bounded list of recent problems, were both shown wrong by TLC before any code was written.

How it made nfltr more reliable

Finding bugs is the visible part. The larger effect is that the guarantees below are now stated once, checked on every push, and tied to the code by traces, so a later change that breaks one fails CI instead of production.

Guarantees now checked before code. Each is an invariant of a spec that TLC checks on every push, with a mutant of the old behaviour that it must catch:

Layers that rely on the layer below. Because link's interface spec states what a session guarantees, the relay core's spec models link in a few lines instead of copying its state machine, and its states stay small enough for CI. When the relay core found that a session could end cleanly while its tail was still in a dead connection, the fix went into link's interface and its code, so every user of link has it, and a refinement check keeps link's full spec within that interface.

Code and spec kept in step. Traces from the ordinary test suites are checked against the specs nightly, and a quick slice on every push. They have caught code that drifted from a correct spec (link's pool held two connections with a maximum of one, because a drain's reservation was split across two locks; link delivered data that arrived after the reader had refused the session, rejected in 12 of 30 traced runs before the fix and 0 of 30 after) and specs that drifted from correct code (a merged hub and node trace rejected because the spec dropped a message the relay does deliver after a node restart; the spec was fixed).

Design first, then code. For each fix above the order was: the spec reproduces the bug as a mutant, the design is changed in the spec until TLC passes and the mutant is caught, then a Go test that fails on the old code, then the code. The rolling-drain fix is a complete example:

What reliability looks like from outside. These runs check the same properties with real processes and real faults. They are not caused by TLA+ alone; the network-fault runs predate the specs:

Trace validation

A spec is our reading of the code; trace validation is how we find out where that reading is wrong. Counts as recorded in the spec READMEs:

Rejected traces found real bugs (a pool past its maximum, data buffered after a refusal was read) and spec bugs (a spec stricter than the protocol). They also found test bugs: tests that move a clock the recorder cannot see, or rewrite state files between steps.

What it did not catch

• Bugs first seen as flakes or failed end-to-end runs. An aborted session ending cleanly (a CI flake), a reconnecting agent's open refused (a flake, red 4 times in two days), a fast reconnect losing a resume, a request failing during a rolling deploy (1 failed visit), and the drain example above. In each, the spec held but had modelled two code steps as one, or left out a message. The fix was to split the action, add the mutant, and then fix the code. A spec is only as fine-grained as the code steps it names.
• A bug the trace model hid. The revocation journal's missed insert was assumed away by the way the trace spec read the journal; an independent review found it.
• A vacuous configuration. link's crash configuration never crashed until a witness property said so. Witnesses now exist for most specs, but not all.
• Time. TLC has no wall clock. Timer bounds, latency and starvation are modelled as discrete ticks at best; a goroutine leak was found by a leak check, and timing flakes by starving the machine.
• Small configurations. Two sides, one or two agents, one crash. A bug that needs three replicas and two crashes is not excluded.
• Open items. The directory's read-then-write operations in Redis leave windows of one round trip (they need a compare-and-set in the store); some specs have no trace recorder yet; model-based replays exist for few specs. And at the time of writing, one nightly hub check has been red for two nights: a mutant of the hub and node monitor protocol is no longer caught by the larger configuration. We have not looked at it yet.

What it costs

Rerun it

link, the relay SDK and the relay core are public. Each needs Go and a JRE; scripts/fetch-tla.sh downloads a pinned tla2tools.jar (link's also a pinned JRE when none is installed) into a cache outside the repository.

git clone https://github.com/nfltr/link && cd link
make spec-invariants   # what CI runs: invariants, the crash config, refinement
make spec-mutants      # every mutant, witness and bad trace must be caught
make spec-traces       # the Go tests with -tags linktrace, each trace checked by TLC

In github.com/nfltr/relay, make spec spec-mutants spec-cltraces; in github.com/nfltr/relay-core, make spec spec-mutants and make spec-traces. Each spec/README.md explains the model, the action-to-function map, the findings and the measurements. The relay server's and the hub's specs are in closed repositories; this post describes them.

Is it for you?

Fits if you write Go code where two goroutines, processes or machines share a state machine and a bug would lose, duplicate or reorder data without an error: a protocol, a lease, a queue with acknowledgements, a cache that must honour a revocation. Start with one spec of the piece you trust least, keep it under a few hundred lines, and add a mutant for the last bug you fixed there. If TLC cannot tell the bug from the fix, the spec is not yet saying anything.

Not ready for a guarantee that the code is correct. A spec checks a small configuration of our reading of the code; trace validation checks only the runs our tests produce. It found many bugs that tests missed and missed several that tests found, so we run both.

Try next: read link's spec/README.md beside Link.tla, then the process post for the tests and fault injection around it, and the link post for what the multiplexer does.