You can't unit test a distributed protocol, but you can model check it

You can’t unit test a distributed protocol. A unit test runs one process on one machine in one order. Your protocol runs ten processes across five machines in an order you don’t control. The gap between those two realities is where your bugs live.

Model checking closes that gap. It explores every possible interleaving of every possible state your protocol can reach. If there’s a way for two replicas to disagree, a way for a leader election to deadlock, or a way for a split-brain scenario to emerge, a model checker will find it. And it will find it before you’ve written the first RPC handler.

Why distributed bugs survive traditional testing

State explosion is the problem. Three nodes exchanging messages can produce billions of execution paths. Hand-written integration tests cover maybe a dozen of them, usually the happy path and a couple of obvious failure modes. The bug where node A crashes exactly between sending a prepare and an ack? Good luck hitting that in CI.

Formal verification sounds like an academic exercise, but model checking is different. You don’t prove the protocol correct for all time. You describe the protocol in a specification language, define the properties you care about, and let a tool exhaustively search the state space up to some bound. When it finds a violation, it hands you a minimal trace. You get a step-by-step recipe for reproducing the bug. No heisenbugs. No “works on my machine.”

The most practical tool for this is TLA+, developed by Leslie Lamport. It looks like math because it is math. But the math is simpler than you expect, and the payoff is finding bugs that would otherwise surface at 2 AM in production.

What model checking actually does

A model checker takes three inputs: a description of your system, a description of its environment, and the properties you want to hold. The system description captures your protocol logic. The environment description captures everything you don’t control: network delays, message loss, node crashes, clock skew. The properties are usually invariants (“the committed log is never overwritten”) or liveness conditions (“every request eventually gets a response”).

The checker then generates every reachable state and every valid transition between them. It does this exhaustively for finite state spaces, or with bounded exploration for infinite ones. If an invariant is violated, it stops and reports the shortest path to the failure.

This is brute force, not magic. The model checker doesn’t understand your intent. It simply tries everything. That is exactly the point. Your integration tests are biased by your assumptions. The model checker has no assumptions.

Specifying a simple consensus protocol in TLA+

Let’s look at a minimal example: a single-decree consensus protocol where a leader proposes a value and a quorum of acceptors must accept it before the value is chosen. This is the core idea behind Paxos, Raft, and every other consensus algorithm you’ve heard of.

Here’s the TLA+ spec for the system:

------------------------------ MODULE Consensus ------------------------------
EXTENDS Integers, Sequences, FiniteSets

CONSTANTS Values, Acceptors, Quorum

VARIABLES chosen

Init == chosen = {}

Propose(v) ==
  /\\ v \\in Values
  /\\ chosen = {}
  /\\ chosen' = {v}

Next ==
  \\E v \\in Values : Propose(v)

Spec == Init /\\ [][Next]_chosen /\\ WF_chosen(Next)

ChosenUniqueness ==
  Cardinality(chosen) \\leq 1
=============================================================================

This spec says: initially nothing is chosen. A propose action can set chosen to a single value, but only if nothing has been chosen yet. The ChosenUniqueness invariant states that at most one value can ever be chosen.

The TLA+ model checker, TLC, will verify that no execution trace violates ChosenUniqueness. If you introduce a bug where two leaders can propose simultaneously without checking for prior values, TLC finds the counterexample in milliseconds.

Adding the messy parts: crashes and message loss

The spec above is too clean. Real distributed systems aren’t clean. Messages get dropped. Nodes reboot. Network partitions isolate groups of nodes from each other. The model only becomes useful when you model these failures.

Here’s a more realistic fragment that models message passing with potential loss:

VARIABLES msgs, acceptorState

Send(m) == msgs' = msgs \\cup {m}

Deliver(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ acceptorState' = [acceptorState EXCEPT ![m.to] = @ \\cup {m.value}]

Drop(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ UNCHANGED acceptorState

Next ==
  \\E m \\in msgs : Deliver(m) \\/ Drop(m)

Drop is the important addition. It models message loss without changing the acceptor state. TLC will explore traces where any message is delivered, dropped, or delayed indefinitely. When you add a leader crash and recovery, the state space grows, but TLC still explores it systematically.

This is the part that tripped me up when I first started with TLA+. I wanted to model only the protocol logic. But the bugs weren’t in the logic. They were in the interaction between the logic and failure modes I hadn’t considered. You have to model both.

The trade-off: state space explosion and abstraction

Model checking is not free. The number of states grows exponentially with the number of processes and the size of your message payloads. A spec with five values and three acceptors might generate millions of states. Add a fourth acceptor and you’re into billions. Run this on your laptop and it will run out of memory before it finishes.

The solution is abstraction. You don’t model your actual 64-byte values. You model two values: V1 and V2. If the protocol behaves correctly for two values, the specific values don’t matter. You don’t model a 10,000-entry log. You model a log of depth 2. If safety holds for depth 2, it almost always holds for arbitrary depth. This is called small-model checking, and it’s the standard practice in the field.

The key skill is learning which details matter and which don’t. Message contents usually don’t matter for safety properties. Message ordering almost always does. Node identities might not matter, but the count of nodes in each role does.

If the state space is still too large, you have other options. You can use symmetry reduction to treat identical nodes as interchangeable. You can bound the depth of the search. Or you can switch to a symbolic model checker like Apalache, which uses SMT solvers to reason about states without enumerating them all.

From spec to implementation: keeping them in sync

A verified spec is worthless if your implementation diverges from it. The spec is the blueprint. The code is the building. There’s no automated bridge between the two, and that gap is where bugs creep back in.

The practical approach is to treat the TLA+ spec as a design document that happens to be executable. Review it alongside the code during pull requests. When the implementation handles an edge case, ask whether the spec handles it too. When you find a bug in production, check whether the spec would have caught it. If not, update the spec.

Some teams go further and generate test cases from the counterexamples TLC produces. A TLC trace showing how two replicas diverge becomes an integration test scenario. This is manual work, but it connects the formal model to your test suite.

At Sentry, we used this approach to validate a distributed rate-limiting protocol. The spec caught a liveness issue where a recovering node could starve in a specific partition scenario. Our integration tests had never triggered it because they always healed partitions cleanly. The model checker didn’t care about clean. It tried the messy case, found the bug, and saved us a very confusing incident.

Getting started: your first model check

If you want to try this, start with the TLA+ toolbox. It’s a free IDE for writing and checking specs. Work through the Paxos and Raft examples that ship with it. They’re more complex than the consensus snippet above, but they show how real protocols are modeled.

For your first spec, pick something small from your own system. A leader election protocol. A distributed cache invalidation scheme. A two-phase commit variant. Write down the invariants you believe hold. Then let TLC tell you whether you’re right. It usually says no, and it usually says it within the first hour.

Model checking won’t find every bug. It won’t help with performance, it won’t catch serialization mistakes, and it won’t verify your implementation matches your spec. What it does is find the deep protocol bugs that integration tests miss, and it finds them at design time, when fixes cost nothing.

That’s the cheapest bug fix in distributed systems. Not a better debugger. Not more monitoring. Catching the bug before the code exists at all.