Our model said everything passed. It was checking nothing.

Felix has a TLA+ model of how a shard replicates, fails over and recovers. CI runs TLC, the TLA+ model checker, over 107 configurations of it. 53 are expected to pass. The other 54 are expected to fail with a specific invariant.

I once watched a change turn four of those configurations into runs that stopped after five states. Normally they explore six or seven million. The two that were meant to pass still passed. The model had stopped saying anything, and the passing checks couldn't tell me.

That was one of three times a check of ours passed without checking anything. Here's how each happened, and what catches them now.

What TLC does, and why a pass can mean nothing

A TLA+ spec describes a system as states and steps. A state is one value for every variable: who leads, what each broker's log holds, which records were acknowledged. A step, called an action, says how one state can turn into the next, like “the leader appends a record” or “a follower crashes”.

An invariant is something that must be true in every state. Ours include AckedSurvive: whoever is serving holds every record a client was told is durable. TLC starts from the initial states, applies every enabled action in every order, and checks each invariant in each state it reaches. A configuration (.cfg) fixes the bounds: three brokers, at most one or two writes, how far the clock runs, which features are on.

If TLC finds a state that breaks an invariant, it prints a counterexample: the exact sequence of steps that gets there. If it runs out of new states first, it reports success.

That last part is the trap. TLC proves the invariant holds in every state it reached. If the interesting states are never reached, the invariant holds trivially. A model where promotion can't fire will never lose a record during promotion.

TLC gives you some help. It prints how many states it found and how deep it went. It can flag deadlock, a state where no action is enabled. But scripts/check_tla.sh runs TLC with -deadlock, which turns that check off, because a bounded config is supposed to run out of things to do. And the script judges a pass by the absence of a violation, not by the state count. A run of five states and a run of six million both come out green.

Story one: the Figure 8 runs that stopped at five states

Raft's Figure 8 is a well-known way to lose a committed entry: a new leader counts a record it inherited from an old term as committed, and a later leader overwrites it. Felix avoids it with a generation-start record. Each new leader writes one at the start of its generation, and nothing it inherited counts as acknowledged until that record does.

The model checks this from a seeded history. FelixShardFigure8.tla starts two leaderships in, because each promotion costs a lapsed lease and the time-bounded runs can't get that far. Four configs start from that history. Two pass with the start record, and each has a twin without it that must violate AckedOnMajority.

#1282 taught the leader to learn each follower's incarnation over its connection. In the model, a report now stores incarnation plus one, so that 0 can mean “none”. Placement only promotes a follower whose reported incarnation matches the current one. The seed report wasn't updated with the new encoding:

\* `incs` holds incarnation + 1 (0 is none), so a report seeded from this
\* names every broker at its first registration, as `sids` names its first
\* identity.
NoReport == [holders |-> {}, len |-> 0, drained |-> FALSE, gen |-> 0, sids |-> [m \in Brokers |-> 0],
             incs |-> [m \in Brokers |-> 1]]   \* was |-> 0

ByLeaderReport(r, f) ==
    /\ f \in r.holders /\ f \notin halted
    /\ f \notin restarting
    /\ IF StorageIds /\ registered[f] /= 0
       THEN r.sids[f] + 1 = registered[f]
       ELSE StampIncarnations => r.incs[f] = inc[f] + 1

With the old seed, every broker in the starting report had “no incarnation”. ByLeaderReport was false for everyone, so no promotion could fire, and each seeded run ended after five states with nothing left on the queue. FelixShardFigure8 and FelixShardFigure8FollowerAcks, normally 5.99M and 7.67M distinct states, passed. The two CutOver configs start from a different history and ran normally.

What failed was the twins. Each twin is its passing config with one setting flipped, and its header says what TLC must find:

\* FelixShardFigure8FollowerAcks.cfg without the generation-start record,
\* so the mark counts a record the leader inherited. `check_tla.sh` expects
\* TLC to lose an acknowledged record (AckedOnMajority): c, promoted at 3,
\* takes x from a in its fence and acknowledges it once a and c answer for
\* it; a promoted at 4 finds b's log ahead by generation and takes y in
\* place of x. Raft's Figure 8, with follower acks in place of the report.
\* About 50K distinct states to the violation, under a second.
...
    StartRecord = FALSE

After the change, FelixShardFigure8NoStartRecord and FelixShardFigure8FollowerAcksNoStartRecord found nothing. CI printed FAIL: expected TLC to violate AckedOnMajority, and the five-state count sat right above it. The fix was one character in the seed.

Story two: a crash that always lost something

When a leader crashes under Felix's relaxed fsync modes, it can lose records it hadn't synced. It comes back under a new storage identity, gives up the shard, and probes its followers. Placement promotes a follower that's level with it or ahead. Only when every follower is behind does it name the old leader again at a new generation. The model calls that step Reclaim.

FelixShardLeaderCrashReclaim.cfg checks it with one write. Its twin, FelixShardLeaderCrashReclaimBlind.cfg, reclaims without measuring the followers and violates AckedSurvive. Both behaved as expected, and the pair was still empty.

The Crash action chose a surviving prefix with \E k \in 0..(Len(log[f]) - 1), so a crash always dropped at least one record. With MaxWrites = 1, the crashed leader always came back empty. An empty log can't be ahead of anyone, so the guard that every follower is behind could never hold, and Reclaim never fired. The pass was vacuous.

The twin didn't catch it because it failed through a different step. ReclaimBlind skips the measurement, so it fires without the guard and loses the record. That proved the measurement mattered. It didn't prove the real Reclaim was reachable.

The fix, in #1315, was to let a crash lose nothing: \E k \in 0..Len(log[f]). That's also more faithful. A SIGKILL keeps the page cache, so a killed broker often loses nothing, and its unclean restart still rotates the identity. Now the leader can come back holding a record no follower took. The PR worked by hand a six-step path from the initial state to a firing Reclaim.

Story three: the config we couldn't afford

The third is a pass we gave up on knowingly.

#1294 made a follower that crashes under a relaxed fsync mode come back under a new storage identity. FelixShardCrashKeepsId.cfg shows why: without the rotation, the follower stays counted on a record it lost, and TLC finds the AckedSurvive violation in seconds.

The passing config needed two writes. With one, a crash either empties the log, which FelixShardWipeFull.cfg already covers, or loses nothing. A partial loss, keeping the first record and dropping the second, needs two. The first attempt, FelixShardCrash.cfg, ran two writes with the clock stopped at 2 and no margin. It started at 08:09 and was still running when the 60-minute PR job was cancelled.

We dropped it. The config header and the README now say plainly that the passing case with a partial loss isn't model-checked in CI. The rotation itself is covered by a unit test the twin cites (a_crash_under_a_relaxed_fsync_mode_rotates_the_id) and by a cluster test, a_crashed_follower_is_not_promoted. That's real coverage, but it isn't the exhaustive check the model would give.

I'd rather have a written gap than a smaller config that passes for the wrong reason, like the one-write version would have.

Why it matters

The docs make specific claims about Felix. A record acknowledged under Quorum survives a leader failover. A crashed leader never comes back without records it acknowledged. Those claims rest partly on these configs. If a config passes without reaching the states it's about, the claim has nothing behind it, and nobody notices until a cluster loses a record.

The empty passes looked exactly like real ones: green CI, no warnings, a “Finished” line. The only difference was a state count nobody was reading.

What we learned

A violating config is the model's smoke detector. A passing config can't tell you it's empty, but a twin that stops violating can. The Figure 8 bug was caught only because the twins existed and check_tla.sh holds them to their expected invariant, not just to “something failed”.

A twin is only as good as the step it fails through. The Reclaim twin removed the measurement and failed. That didn't show the guarded step could ever fire. #1328 got this right: FelixShardSuspicionWipeUnbacked.cfg differs from the passing FelixShardSuspicion.cfg only by the new Forget step, so its violation has to go through it.

Bounds bite in both directions. One write made the crash model cheap enough to check, and it also made the interesting crash impossible. The model's choices about what a fault can do need the same scrutiny as the code's.

Finally, the model and the code drift apart unless something forces them together. Early on, a protocol change (#268) shipped without touching the model, and for three weeks CI pinned a violation the code no longer had. So scripts/check_spec_pairing.py fails any PR that touches the code the model describes but not a .tla or .cfg beyond comments. The way out is a Spec-Unaffected: <reason> line in a commit message or the PR description. It's blunt on purpose. Most edits to those files don't change the protocol, but nobody changes the protocol without being asked.

The rule that goes with it: when the model and the docs disagree, we don't edit the model to match. We fix the code, or we keep the model's finding as an expected violation and open an issue.

What we'll do differently

Every passing config gets a violating twin that differs by one fix, and the twin must fail through the step that fix guards. If the twin can fail some other way, it doesn't count.

Every new action gets a reachability check before it merges. Add a temporary invariant that says the action never fires, and TLC must violate it. The README already did this once for acknowledgements: a temporary acked = {} invariant that TLC breaks in 2,307 states. Doing it by hand in a PR description isn't enough.

Cfg headers record their state counts, and a run that drops far below its recorded count should fail, not just pass quietly.

The cost is time. The 107 configs are split across seven parallel CI jobs. check_tla.sh fills them longest first, using minutes measured from earlier CI runs, so one long config doesn't push a job past its hour. Pull requests run the configs of ten minutes or less, plus any whose .cfg changed. Main runs all of them. When a config won't fit, like FelixShardCrash, we write down the gap rather than shrink it until it means nothing.

Trying it

The specs and every configuration are in docs/formal/, with a README that lists what each config checks and what it's expected to do. Each .cfg header says what it models and cites the tests that back its assumptions.

To check one config, from the repo root:

scripts/check_tla.sh FelixShardFigure8FollowerAcksNoStartRecord

That needs Java 11 or later, or Docker or Podman. It fetches the TLA+ tools once, pinned by version and checksum, and holds the config to its registered outcome. task tla:check runs all of them. Look at the distinct states found line, not just the verdict.

To run Felix itself, the Docker Compose guide starts a control plane and a broker with docker compose up -d (or podman compose).

docker compose up -d