Formal Verification

A formal model of one shard

FelixShard.tla is a TLA+ model of the protocol in docs/replication-design.md: the lease that lets a broker serve a shard, the replication that puts its records on a majority, and the promotion that names the next leader when the lease lapses. TLC checks it in about a minute, and task tla:check runs it locally and in CI.

Prose about a safety interval is an argument; a model checker either finds the interleaving that breaks it or runs out of interleavings to try. This one found something the prose had not.

What is modelled

One shard, three brokers, one control plane, discrete time.

• Clocks. now is real time. Each broker's clock is monotonic and within Drift of real time, which is the design's drift-rate assumption in the only shape a finite model needs. On each tick a broker's clock moves by zero, one or two: standing still is slow, two is fast.
• Leases. The leader heartbeats; the control plane accepts a heartbeat only while the lease it granted has not lapsed, and extends it by L. The broker extends its own belief from the instant it sent the heartbeat, on its own clock, and stops serving Eps before that belief expires. Heartbeats can be lost. The control plane grants the next generation no earlier than Margin after the expiry it recorded.
• Writes. Admission checks the lease. Commit checks it again, or not, which is the CheckAtCommit knob. Anything may happen between the two: that gap is where a paused process lives.
• Replication. The leader ships the next record a follower is missing. A follower whose log disagrees with the leader's keeps what a newer generation than its own last accepted one says, above its high-water mark; anything else halts it. A follower refuses a leader older than one it has heard from.
• Acknowledgement. Under Quorum, once a majority including the leader holds the record; under Leader, on the leader's own commit.
• Reports. The leader tells the control plane which followers hold every record it does. The report travels on its own: it may arrive after the acknowledgements it describes, or never.
• Promotion. After the lapse and the margin, the control plane names a new leader. Promotion = "leader-report" is the design as written: a follower the last report named as caught up. Promotion = "log-order" is the live replica with the greatest (last generation, length): Raft's election restriction, which needs no report.

Not modelled: the storage layer (a commit is a commit), network partitions as such (they are lost heartbeats, lost reports, and delays), retention, and the bootstrap of a follower below the leader's base.

What is checked

Invariant	Says
AtMostOneServing	No two brokers serve the shard at once.
AckedSurvive	Whoever is serving holds every acknowledged record.
AckedAgree	Two brokers never hold different acknowledged records at one offset.
AckedOnMajority	Every acknowledged Quorum record is on a majority.
NoTruncationBelowHwm	A follower never discards a record below its high-water mark.
NoStaleCommit	No broker commits at a generation the control plane has superseded.

The configurations, and what each must do

scripts/check_tla.sh holds each configuration to a declared outcome. A configuration that must find a violation exists to show a check is load-bearing, or to pin a finding the design has not acted on yet; a violation that quietly became a pass would be a model that stopped saying anything.

Configuration	Knobs	Must
FelixShardLease.cfg	drifting clocks, no writes: heartbeats, lapses, promotions	pass AtMostOneServing and NoStaleCommit (1.0M states)
FelixShardLogOrder.cfg	both lease checks, Quorum, two writes, promotion by log order	pass every invariant (3.0M states)
FelixShardThinMargin.cfg	drifting clocks with Margin = 0 and Eps = 0	violate AtMostOneServing
FelixShardNoCommitCheck.cfg	commit-time lease check removed	violate NoStaleCommit
FelixShardNoReportOrder.cfg	the design before #268: a Quorum ack released before the report describing it lands	violate AckedSurvive
FelixShard.cfg	the design as implemented: report-before-mark, promotion from the leader's report	pass every invariant (2.4M states)

Drift is checked where it matters and nowhere else. The lease configurations carry drifting clocks and no writes, so every interleaving of three drifting clocks is affordable; the replication configurations carry writes and synchronised clocks, because nothing about which replica holds which record depends on what time a broker thinks it is. One configuration with both ran past four hundred million states without finishing.

What ties this to the code, and what does not

A spec and an implementation are two artifacts in two languages. Nothing in the toolchain makes one follow the other, and the gap is not hypothetical: the broker gained the report-before-mark ordering in #268, this model went on describing the design without it, and check_tla.sh pinned the resulting AckedSurvive violation as expected — asserting for three weeks that Felix loses acknowledged records, for a design it no longer had. An issue was then filed against the model's finding, proposing work the code did not need.

So every configuration carries an Evidence: block naming the tests that establish what it assumes of the implementation, and scripts/check_spec_evidence.py (run by task docs:evidence) fails when a cited test no longer exists or a configuration cites nothing. Rename the test for a behaviour and the spec is put in front of you.

A configuration that deliberately models something the code does not do says Evidence: none and why — the counterexample configurations instead cite the test proving the check they remove is really there.

What this does not do. A cited test can keep its name while its assertions change, and the spec can model a behaviour wrongly while every citation resolves. This makes drift harder to introduce silently; it does not detect it. Checking that the implementation conforms to the spec needs trace validation — emitting protocol events and checking recorded runs are behaviours of the spec — which is a different and much larger mechanism. Tracked in #598.

The interval that is load-bearing

With no margin on either side, TLC finds a leader whose clock runs slow still serving when the control plane, whose lease copy has lapsed, names the next one. Margin and Eps together have to outlast what Drift can do to the two clocks, which is the design's safety interval, and removing it is two leaders in one step.

The check that is load-bearing

With CheckAtCommit = FALSE, TLC finds a broker that admits a write while its lease is valid, is paused while the lease lapses and the next generation is granted, and then commits. That is the "process suspension" case the design names, and the second check is what closes it.

The ordering that is load-bearing

With ReportBeforeAck = FALSE, TLC finds this in a second:

1. The leader reports its two followers level with it.
2. It admits and commits a write, ships it to one follower, and acknowledges it under Quorum: leader plus one follower is a majority of three.
3. It dies before the next report leaves. The report the control plane holds is recent, and predates the acknowledgement.
4. The lease lapses, the margin passes, and the control plane promotes the other follower, which the report named as level. It holds no copy of the acknowledged record. AckedSurvive fails.

Report expiry does not close this. The design's expiry is about reports older than the time it takes to notice a leader is gone; this report is fresh, it is just older than the last acknowledgement.

What closes it is ordering, not freshness, and the broker does it: the leader reports who holds the record, waits for that report to land, and only then moves the quorum mark that releases the acknowledgement. That is publish_mark in services/broker/src/replication/driver.rs, which moves the mark only if reported, and await_quorum, which blocks the publish on the mark. With ReportBeforeAck = TRUE — FelixShard.cfg, the implemented design — TLC explores 2.4M distinct states and finds no violation.

So the pair is the point. The ordering is not merely present in the code; the model shows the guarantee fails without it.

A caution on reading a pass. FelixShard.cfg passing is only meaningful if acknowledgements actually happen under the added precondition — a precondition nothing can satisfy would make AckedSurvive vacuously true. Checked by hand with a temporary acked = {} invariant, which TLC violates in 7,107 states: acknowledgements are released, and the pass is about them.

Promotion by log order finds no trace, in the same bounds. A replica holding an acknowledged Quorum record is in every majority that could acknowledge one after it, so the replica with the greatest (last generation, length) among the live ones holds every acknowledged record; the generation comes first because a stale proposal from an older leader can be longer than the log that superseded it. That rule needs each replica to say where it is — a position on its own heartbeat — rather than the leader to say where its followers were.

Running it

task tla:check          # java or docker; fetches the TLA+ tools once, pinned

To explore a configuration by hand, with the trace when a check fails:

java -jar target/tla/tla2tools-v1.7.4.jar -deadlock -workers auto \
  -config docs/formal/FelixShard.cfg docs/formal/FelixShard.tla

The bounds (MaxTime, MaxWrites, and the SYMMETRY over brokers) keep the whole check to about a minute. Widening them widens what is checked; the invariants do not change. The script runs TLC with checkpoints off and its scratch directory outside the tree. Run by hand without -metadir, TLC writes a states/ directory beside the spec that reaches gigabytes; .gitignore covers it.

---

Generated from docs/formal/README.md in the repository. That file is the source of truth; this page may be behind it.