23. Verifying Distributed Systems

"How do you know your design is correct?" is a standard senior-level follow-up, and the honest answer is never "unit tests". Distributed systems fail in interleavings that example-based tests almost never produce: a message delayed past a lease expiry, a crash between two writes, a partition during a leader election. This section covers the verification toolbox from cheapest to strongest, and how real companies use it.

23.1 The verification ladder

                       Strength of guarantee ▲            Cost / expertise ▲
 ┌──────────────────────────────────────────────────────────────────────────────┐
 │ 7. Formal specification & model checking (TLA+, P)  — design-level proofs     │
 │ 6. Deterministic simulation testing (DST)           — real code, simulated world│
 │ 5. Linearizability / consistency checking (Jepsen)  — black-box, real faults   │
 │ 4. Fault injection & chaos engineering              — staging and production   │
 │ 3. Property-based & model-based testing             — random inputs vs model   │
 │ 2. Integration tests with real dependencies         — happy + known failures   │
 │ 1. Unit tests                                       — logic in isolation       │
 └──────────────────────────────────────────────────────────────────────────────┘
 Plus, always, in production: invariant checkers, reconciliation, canary analysis, shadow traffic

You don't use all of them everywhere. Match the rung to the cost of being wrong: a ledger, a consensus protocol, or a storage engine justifies rungs 5–7. A CRUD service needs rungs 1–4 plus production checks.

23.2 Property-based testing (rung 3)

Instead of hand-written examples, state a property that must always hold and let the framework generate thousands of random inputs, then shrink any failure to a minimal counterexample. In Go, use the standard library's testing/quick, or libraries such as rapid. In Python, Hypothesis.

The key design move is to make time and randomness injectable, so the code is testable without sleeping:

type Clock interface{ Now() time.Time }

type TokenBucket struct {
	capacity, rate, tokens float64 // rate = tokens per second
	last                   time.Time
	clock                  Clock
}

func NewTokenBucket(capacity, rate float64, c Clock) *TokenBucket {
	return &TokenBucket{capacity: capacity, rate: rate, tokens: capacity, last: c.Now(), clock: c}
}

func (b *TokenBucket) Allow() bool {
	now := b.clock.Now()
	b.tokens = math.Min(b.capacity, b.tokens+now.Sub(b.last).Seconds()*b.rate)
	b.last = now
	if b.tokens >= 1 {
		b.tokens--
		return true
	}
	return false
}

type fakeClock struct{ t time.Time }

func (f *fakeClock) Now() time.Time { return f.t }

// Property: for ANY sequence of request timings, the number of allowed requests
// never exceeds capacity + rate × elapsed time.
func TestTokenBucketNeverExceedsBudget(t *testing.T) {
	prop := func(gapsMs []uint16) bool {
		clk := &fakeClock{t: time.Unix(0, 0)}
		const capacity, rate = 10.0, 5.0
		b := NewTokenBucket(capacity, rate, clk)
		start, allowed := clk.t, 0
		for _, g := range gapsMs {
			clk.t = clk.t.Add(time.Duration(g%500) * time.Millisecond)
			if b.Allow() {
				allowed++
			}
		}
		elapsed := clk.t.Sub(start).Seconds()
		return float64(allowed) <= capacity+rate*elapsed+1e-9
	}
	if err := quick.Check(prop, &quick.Config{MaxCount: 10000}); err != nil {
		t.Fatal(err)
	}
}

Model-based testing extends this to stateful systems: generate random sequences of operations, apply them to the real system and to a simple in-memory reference model, and assert they agree. AWS used this approach heavily for ShardStore, a storage node for S3 ("Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3", SOSP 2021), including crash and recovery points in the generated sequences.

23.3 Deterministic simulation testing (rung 6)

The idea: run the real production code in a single-threaded simulator where the network, disk, clock, and randomness are all simulated and driven by one seed. The simulator injects faults (partitions, crashes, slow disks, clock jumps) far more often than reality does, and any failure can be replayed exactly from its seed.

// Everything nondeterministic goes through Env, so one seed reproduces a run exactly.
type Env interface {
	Now() time.Time
	Rand() *rand.Rand
	Send(from, to NodeID, msg Message) // simulated network: may delay, drop, reorder, duplicate
	After(d time.Duration, fn func())  // simulated timers on a virtual clock
}

func RunSimulation(seed int64, steps int) error {
	sim := NewSimulator(seed)          // single-threaded event loop with a virtual clock
	cluster := NewCluster(sim, 5)      // the REAL node code, wired to sim instead of the OS
	workload := NewRandomWorkload(sim) // clients issuing reads/writes with recorded history
	for i := 0; i < steps; i++ {
		sim.MaybeInjectFault() // partition, crash/restart, clock jump, disk error
		sim.Step()             // deliver the next event in virtual-time order
		if err := cluster.CheckInvariants(); err != nil {
			return fmt.Errorf("seed=%d step=%d: %w", seed, i, err) // rerun the same seed to debug
		}
	}
	return workload.CheckLinearizable() // e.g. with a Porcupine-style checker (§23.4)
}
// CI runs thousands of seeds per commit; nightly jobs run millions.

Who does this: FoundationDB made deterministic simulation the center of its engineering, and is often cited as the reason it was famously robust. TigerBeetle (a financial database) runs its "VOPR" simulator continuously. Antithesis, founded by former FoundationDB engineers, offers deterministic simulation of whole containerized systems as a service. The price: the code must be designed for it from day one (no direct OS calls, goroutines, or wall-clock reads outside the Env abstraction). Retrofitting is hard, and that's an architecture decision.

23.4 Consistency checking under real faults: Jepsen-style (rung 5)

Black-box testing of a real cluster: run concurrent clients, inject real faults (network partitions with iptables, process kills, clock skew), record the history of every operation with its invocation and completion times, then check whether that history is consistent with the claimed model.

// Sketch based on github.com/anishathalye/porcupine (a linearizability checker in Go).
// Check the library's current API before use.
type kvInput struct{ op, key, value string } // op: "get" | "put"
type kvOutput struct{ value string }

var registerModel = porcupine.Model{
	Partition: partitionByKey, // check each key independently: much faster
	Init:      func() interface{} { return "" },
	Step: func(state, input, output interface{}) (bool, interface{}) {
		in, out := input.(kvInput), output.(kvOutput)
		if in.op == "get" {
			return out.value == state.(string), state // a read must return the current value
		}
		return true, in.value // a put sets the value
	},
}

// history: []porcupine.Operation{ {ClientId, Input, Call, Output, Return}, ... } recorded under faults
// ok := porcupine.CheckOperations(registerModel, history)

Jepsen (Kyle Kingsbury) uses checkers such as Knossos (linearizability) and Elle (transactional isolation anomalies). Its public analyses found violations of documented guarantees in many well-known databases, from lost acknowledged writes to stale reads under partitions. Before you rely on a database's consistency claim, read its Jepsen report (§10.7).

23.5 Formal methods: specifying the design itself (rung 7)

Model checking verifies the design (the algorithm) by exhaustively exploring every interleaving of a small model, which is where the subtle bugs live, before any code exists.

A tiny TLA+ example: a two-step transfer (like a saga, §12) and the invariant people wrongly assume:

------------------------------ MODULE Transfer ------------------------------
EXTENDS Integers
VARIABLES alice, bob, pc

Init == alice = 10 /\ bob = 10 /\ pc = "start"

Withdraw == /\ pc = "start"
            /\ alice >= 5
            /\ alice' = alice - 5
            /\ pc' = "withdrawn"
            /\ UNCHANGED bob

Deposit ==  /\ pc = "withdrawn"
            /\ bob' = bob + 5
            /\ pc' = "done"
            /\ UNCHANGED alice

Done == pc = "done" /\ UNCHANGED <<alice, bob, pc>>

Next == Withdraw \/ Deposit \/ Done
Spec == Init /\ [][Next]_<<alice, bob, pc>>

TotalConserved == alice + bob = 20                       \* VIOLATED

InFlightAware ==                                          \* holds
    /\ (pc = "withdrawn")  => (alice + bob = 15)
    /\ (pc /= "withdrawn") => (alice + bob = 20)
==============================================================================

The model checker (TLC) immediately finds a counterexample to TotalConserved: the state alice = 5, bob = 10, pc = "withdrawn". That's the saga isolation gap (§12.7) in four lines. Real specs model crashes, retries, and concurrent transfers, and find bugs that need dozens of steps to trigger.

Who uses it:

• AWS, "How Amazon Web Services Uses Formal Methods" (Communications of the ACM, 2015): engineers used TLA+ on DynamoDB, S3, EBS, and internal lock managers, and found subtle bugs that had passed design review, code review, and testing. AWS has since described using the P language for distributed protocols as well.
• Microsoft created P and used it for the Windows USB 3.0 driver stack. TLA+ has been used for Azure Cosmos DB's consistency models (TLA+ itself came from Leslie Lamport, who was at Microsoft Research).
• When to propose it in an interview: for consensus, replication, distributed locks and leases, payment state machines, and cache-invalidation protocols. "I'd write a TLA+ spec of the failover protocol before implementing it" is a credible Staff+ answer for those.

23.6 Fault injection & chaos engineering (rung 4)

The principle: start with a hypothesis ("checkout keeps p99 < 800 ms if the recommendations service is down"), minimize the blast radius, and automate the abort.

23.7 Verifying in production (always on)

Tests can't cover reality. Production verification catches what slipped through:

• Invariant checkers / auditors: background jobs asserting business invariants (every ledger transaction balances; every PAID order has a capture; replica checksums match).
• Reconciliation against an independent source of truth (bank settlement files, §39; stream vs batch, §44).
• Automated canary analysis: statistical comparison of canary vs baseline metrics before promotion. Netflix and Google open-sourced Kayenta (2018) for this.
• Shadow traffic and differential testing: run the new implementation on real requests and compare outputs (GitHub Scientist, §29.6).
• Synthetic probes that exercise critical user journeys every minute (§16).

23.8 Corner cases & pitfalls

• Tests depending on real time (sleep(100ms)) are slow and flaky. Inject clocks.
• Faults that never hit the dangerous window: randomly killing a process every 10 minutes rarely lands between "write DB" and "publish event". Use targeted fault points (crash at step N) plus simulation.
• Simulation fidelity gaps: the simulator's disk never returns torn or partial writes, but real disks and firmware do. Model the failure modes the hardware really has.
• Spec–code drift: the TLA+ spec verified version 1 of the protocol, and the code is now at version 4. Keep specs in the repository, review them with protocol changes, or generate test cases from the model.
• Checker cost: linearizability checking is NP-complete in general. Partition the history (per key) and keep histories bounded.
• Production checks that page nobody: an invariant violation must be an alert with an owner, not a log line.