A Formal Verification Of The Paxos Protocol With Informal Proof And Coq Implementation

The Juggling Chainsaw: Why We Must Formally Verify the Protocols Running Our World

(Intro as given, ends with “A proposer suggests a value. A set of acceptors …”)

… acceptors accept the value, and a learner learns what value was chosen. Simple, right? But the devil—as always in distributed systems—lives in the concurrency, the failures, and the asynchrony. This blog post is not a tutorial on Paxos. It is a deep dive into why even a “simple” protocol like Paxos is terrifyingly subtle, and how we can use the most rigorous tool in computer science—formal verification with the Coq proof assistant—to build an unbreakable argument for its correctness. We will walk through the informal proof, see where human intuition fails, and then witness how Coq can encode the entire protocol as a mathematical object and prove its safety and liveness properties without any shadow of a doubt.

By the end, you will understand why the nuclear reactor analogy is not an exaggeration. When a consensus protocol controls the ordering of financial transactions or the timing of safety-critical operations, a single bug can cascade into catastrophe. Formal verification is the only way to guarantee that the juggling chainsaw never drops.

1. A Quick Refresher: The Paxos Protocol

Before we can verify Paxos, we must understand it intimately. Lamport’s original description used a parliament of Greek senators, but we’ll use a more modern analogy: a group of friends trying to decide where to eat for dinner.

The Scenario: Three friends – Alice, Bob, and Carol – want to agree on a restaurant. They can’t meet in person; they can only send text messages. Messages can be delayed, lost, or duplicated, and any friend might suddenly fall asleep (crash) and later wake up (recover). They need a protocol that guarantees that even with these chaotic failures, they will all eventually agree on the same restaurant, and that restaurant will be one that was actually proposed by someone.

This is the consensus problem. Paxos solves it in a series of phases. Let’s define the roles:

• Proposer: A process that proposes a value (e.g., Alice suggests “Pizza Palace”).
• Acceptor: A process that votes on proposals. Any process can be an acceptor. The protocol requires that a majority of acceptors agree for a value to be chosen.
• Learner: A process that simply learns what value was chosen. Learners do not participate in voting.

In Paxos, there may be multiple proposers, and they may propose different values concurrently. The magic of Paxos is that even with competing proposals and failures, it guarantees safety (only a single value is ever chosen) and liveness (some value will eventually be chosen if a majority of acceptors remain alive and communication is eventually reliable).

Phase 1: Prepare

A proposer (say Alice) starts by sending a prepare request with a proposal number n to a quorum of acceptors. The proposal number must be unique and monotonically increasing. Typically, proposers use a combination of a round number and their own ID to ensure uniqueness (e.g., (round, id)).

An acceptor, upon receiving a prepare request with number n:

• If n is greater than any proposal number it has ever seen, it promises not to accept any proposal with a number less than n. It also sends back the highest-numbered proposal (if any) that it has already accepted, along with its value. If it hasn’t accepted any, it sends null.
• If n is smaller than or equal to the highest proposal number it has seen, it ignores the request (or sends a rejection, but the standard protocol simply ignores).

After Alice receives responses from a majority of acceptors, she moves to Phase 2.

Phase 2: Accept

Alice now has a set of responses. Some acceptors may have sent back previously accepted proposals. Alice must choose a value to propose in the accept request. The rule is:

• If any acceptor reported a previously accepted proposal, Alice must set her value to the value of the highest-numbered proposal among those reported (the most recent).
• If no acceptor reported any accepted proposal, Alice is free to propose any value (her original suggestion).

Alice sends an accept request with the same proposal number n and her chosen value v to the same quorum (or perhaps a larger set) of acceptors.

An acceptor, upon receiving an accept request with number n:

• If it has not promised to ignore proposals with numbers less than some higher number (i.e., n is still the highest it has seen), it accepts the proposal and records (n, v).
• Otherwise, it ignores the request.

If Alice receives accept acknowledgements from a majority of acceptors, then the value v is chosen.

Learning the Chosen Value

Learners can learn the chosen value by querying acceptors, or by having acceptors broadcast their acceptances. The protocol does not specify this in detail; any reliable broadcast mechanism works.

Why This Works: The Key Invariant

The safety of Paxos relies on two invariants:

1. P1a: An acceptor can only accept a proposal with number n if it has never responded to a prepare request with a number greater than n.
2. P2b: If a proposal with value v and number n is chosen, then every higher-numbered proposal issued by any proposer also has value v.

The second invariant (P2b) is the heart of Paxos. It ensures that once a value is chosen, any future proposal will pick the same value, so no conflicting value can ever be chosen. The proof of P2b is inductive and relies on the fact that the proposer in Phase 2 must use the value of the highest-numbered accepted proposal among the quorum that responded to its prepare. Because any two majorities intersect, the proposer is forced to see the chosen value.

Example Walkthrough

Let’s trace a simple execution. Suppose three acceptors: A1, A2, A3. Proposer P1 proposes value x with number 1. It sends prepare(1) to all three. All three acceptors have never seen any proposal, so they all promise (send back null). P1 now has a majority (three out of three). It sends accept(1, x) to all three. All three accept. Value x is chosen.

Now, a second proposer P2 starts with number 2. It sends prepare(2) to A2 and A3 (majority). A2 and A3 have accepted proposal 1 (x). They promise not to accept any proposal < 2, and send back the highest accepted: (1, x). P2 now must propose x (because it received a previously accepted proposal). It sends accept(2, x) to A2 and A3. They accept. Value x remains chosen.

What if P2 had not received any previously accepted proposal? That could happen if it contacted a quorum that did not include any acceptor that had accepted x (e.g., if only A1 accepted x and P2 contacted A2 and A3, but note: a majority must intersect, so if A1 is the only one that accepted x, and A2 and A3 form a majority, then that majority must include A1? Actually, if there are three acceptors, a majority is two. If A1 accepted x, but A2 and A3 did not (they might have crashed during accept), then the majority {A2, A3} does not include A1, so P2 would not see any previous value. But that would violate the invariant? Let’s check: If A1 accepted x, but A2 and A3 didn’t, then x is not chosen because a majority requires at least two acceptances. So x is not yet chosen. So P2 is free to propose a different value. This is correct. The safety condition only kicks in once a value is chosen (accepted by a majority). Until then, multiple proposals can conflict.

This subtlety is exactly why formal proofs are necessary: human intuition can easily misstep.

2. The Perils of Informal Reasoning

Leslie Lamport provided an informal proof of Paxos in his “Paxos Made Simple” paper. The proof is concise and convincing to a mathematician. But for software engineers implementing the protocol, informal proofs are not enough. We are not dealing with Platonic ideals; we are dealing with network delays, message corruption, and process crashes. The proof assumes certain axioms (e.g., message delivery is reliable after some time, processes have stable storage). Real systems violate these assumptions in tricky ways.

For example, the informal proof of P2b uses the fact that “any two majorities intersect.” But in a system with partial failures, the set of acceptors that respond to a prepare request might not be exactly the same as the set that respond to the subsequent accept request. The protocol requires that the proposer sends accept to the same quorum? Actually, Lamport’s original description says the proposer sends accept to “a set of acceptors” (often the same one). But if the set is different, the intersection property still holds because each set is a majority of the total acceptors; any two majorities intersect. However, a subtle bug arises if the proposer sends prepare to one majority and accept to a different majority, and the acceptance messages themselves might be lost. The proof must account for all possible interleavings.

Furthermore, many implementations of Paxos (like Google’s Chubby, or Zookeeper’s Zab) are actually variants like Multi-Paxos, which introduces leaders and log replication. These variants have additional complexities: leader election, log consistency, epochs, etc. The informal proof of basic Paxos does not directly cover these extensions. Bugs have been found in production systems that stem from violations of the proof’s assumptions.

A famous example is the “Paxos flaw” discovered by Butler Lampson in 2001. He pointed out that in the original Phase 2 rule, a proposer can ignore responses from acceptors that have already accepted a higher-numbered proposal but not yet responded to the current prepare. The fix required an additional rule about ignoring out-of-date responses. This flaw was subtle and existed for years in informal reasoning.

Another example: The implementation of Paxos in the Google Chubby lock service had a bug where a leader could re-propose a value from an old term, violating the invariant that a chosen value must be re-proposed. This was caught only after years of operation.

These examples illustrate that even the smartest engineers can make mistakes when reasoning about concurrent, fault-prone systems. The nuclear reactor analogy is not hyperbole: a bug in the consensus protocol of a stock exchange could trigger a flash crash. Formal verification is the only way to achieve mathematical certainty.

3. Enter Formal Verification: Coq and the Proof Assistant

Formal verification means using mathematical methods to prove that a system satisfies a given specification. Unlike testing, which can only show the presence of bugs, a proof demonstrates their absence (within the model). The most powerful tool for this is a proof assistant like Coq, which allows us to encode the protocol and its properties in a language that the machine can check.

Coq is based on the Calculus of Inductive Constructions (CIC), a typed lambda calculus that supports dependent types. We can define the state of acceptors, the messages, and the transitions as inductive types. Then we can write theorems about invariants and use Coq’s logic to prove them. Coq’s proof engine ensures that every logical step is valid, down to the axioms of set theory.

Why Coq for Paxos? Because Paxos is a state machine with a finite number of possible configurations (when modeling crash-recovery, the state is infinite due to unbounded proposal numbers, but we can use inductive reasoning). Coq excels at inductive proofs. Moreover, the Coq ecosystem has libraries for modeling distributed systems (e.g., the Verdi framework, which provides a formal model of network semantics).

A Minimal Model of Paxos in Coq

Let’s sketch how one would model basic Paxos in Coq. We’ll define:

• ProposalNumber as a natural number.
• Value as a type A (we treat it abstractly).
• AcceptorState as a tuple: (maxPrepareProposal: option ProposalNumber, acceptedProposal: option (ProposalNumber * Value)). Initially, both are None.
• ProposerState might be the current round and the value it is trying to propose.

Messages:

Inductive Msg : Type :=
| Prepare (n : ProposalNumber) (from : AcceptorID)
| Promise (n : ProposalNumber) (prevAccept : option (ProposalNumber * Value)) (to : AcceptorID)
| Accept (n : ProposalNumber) (v : Value) (from : AcceptorID)
| Accepted (n : ProposalNumber) (v : Value) (to : AcceptorID)
| ...

We then define a step function that takes a configuration (state of all processes + network buffer) and produces a new configuration after delivering one message or processing a local event.

The key invariant is: “If a value v is chosen (i.e., exists a proposal (n,v) that is accepted by a majority), then no proposal with a different value can ever be chosen.” In Coq, we express this as a theorem:

Theorem safety : forall (s : SystemState) (n1 n2 : ProposalNumber) (v1 v2 : Value),
  (ChosenIn s n1 v1) ->
  (ChosenIn s n2 v2) ->
  (v1 = v2) \/ (n1 <> n2 /\ ... )  (* actually, exactly that values must be equal if both chosen *)

But the exact statement is: If a value is chosen, then any later value chosen must be the same value. So:

Theorem single_value_chosen : forall (s : SystemState) (v1 v2 : Value) (n1 n2 : ProposalNumber),
  chosen n1 v1 s -> chosen n2 v2 s -> v1 = v2.

Proving this requires an induction on the sequence of steps. The informal proof of P2b becomes a lemma:

Lemma p2b : forall n v s,
  chosen n v s ->
  forall m n' s',
    n' > n ->
    issued n' m s' ->
    (proposedValueIn s' n') = v.

Where issued means the proposer sent an accept request with number n’. The proof uses the fact that the proposer’s value is determined by the majority’s responses, which must include an acceptor that accepted n. This is where the intersection property is encoded.

Modeling Crashes and Recovery

A major challenge is modeling crash-recovery. Coq can handle it by adding a “persistent” state that survives crashes. In the Verdi framework, processes have a “disk” that persists across reboots. We define a transition where a process crashes and later restarts with a log that contains the last proposal number it had promised. The invariants must hold even across restarts. This is notoriously difficult to get right in informal implementations, but Coq can prove it.

We can also model network semantics: asynchronous, unreliable, with duplication and reordering. The Verdi library provides a “network” module that captures all these behaviors. The proof then holds under the worst-case network assumptions.

4. Verifying Paxos in Coq: A Step-by-Step Tour

Let’s walk through a real Coq proof of Paxos safety. I’ll use a simplified version based on the Verdi tutorial by Doug Woos et al. (UPenn).

Step 1: Define the system state.

Record acceptor_state :=
  { n_promise : nat;
    n_accepted : nat;
    v_accepted : option val }.

Here n_promise is the highest prepare number the acceptor has responded to. n_accepted and v_accepted record the highest-numbered proposal it has accepted.

Step 2: Define message types.

Inductive msg :=
| Prepare (n : nat)
| Promise (n : nat) (prev_n : nat) (prev_v : option val)
| Accept (n : nat) (v : val)
| Accepted (n : nat) (v : val).

Step 3: Define the transition function.

We define a step that takes a system configuration (map from acceptor IDs to acceptor_state, plus a multiset of messages) and applies one of three events: a proposer initiates a prepare, an acceptor handles a message, or a proposer initiates an accept (based on promises received). This is a “big-step” style; more refined models use a small-step with explicit process actions.

Step 4: Define the predicate chosen n v config.
A value v with proposal number n is chosen if there exists a set of acceptors S such that:

• |S| > N/2 (majority),
• For every acceptor a in S, a has accepted (n, v) (i.e., n_accepted a = n and v_accepted a = Some v).

Step 5: State the invariant.

The main invariant inv is a conjunction of several lemmas:

• inv1: If an acceptor has accepted (n,v), then its n_promise >= n.
• inv2: If an acceptor has promised for n, it cannot later accept a proposal with number < n.
• inv3: If a proposer issues an accept with number n and value v, then either no acceptor has accepted any proposal < n, or v is the value of the highest-numbered accepted proposal among the quorum that responded.

The last one (inv3) is the heart. In Coq, we formalize it as:

Definition inv3 (cfg : config) : Prop :=
  forall (p : proposerID) (n : nat) (v : val) (quorum : list acceptorID),
    issuedAccept cfg p n v quorum ->
    ((forall a : acceptorID, In a quorum -> highestAccepted cfg a = None) /\ v = proposed_value p) \/
    (exists (a : acceptorID) (m : nat) (w : val),
        In a quorum /\ highestAccepted cfg a = Some (m,w) /\ m = max_among quorum (accepted_numbers cfg) /\
        v = w).

Step 6: Prove that the invariant holds initially and is preserved by every step.

This is done by induction. Each case (e.g., deliver Promise, deliver Accept, crash, restart) must be shown to preserve inv. Coq’s induction tactic and inversion are used extensively.

Step 7: Prove safety from the invariant.

Once we have inv holds for all reachable configurations, we can prove:

Theorem safety : forall cfg n1 n2 v1 v2,
  reachable cfg -> chosen cfg n1 v1 -> chosen cfg n2 v2 -> v1 = v2.

The proof: Suppose both chosen. Since both majorities must intersect, there exists an acceptor a in both quorums. That acceptor accepted both (n1,v1) and (n2,v2). By inv1, an acceptor can only accept one proposal number (the highest). Therefore n1 = n2. By the definition of accept, an acceptor stores only one (n,v) for a given n, so v1 = v2.

Code Snippet: A Lemma from the Proof

Here is a real snippet from a Coq proof of Paxos (adapted from a tutorial):

Lemma accepted_unique : forall cfg a n v,
  reached cfg ->
  acceptor_state cfg a = Some (mk_acc n v (Some (n,v))) ->
  forall n' v',
    acceptor_state cfg a = Some (mk_acc n' v' (Some (n',v'))) ->
    n = n' /\ v = v'.
Proof.
  intros cfg a n v Hreach Hstate n' v' Hstate'.
  rewrite Hstate in Hstate'; inversion Hstate'; auto.
Qed.

This lemma says that once an acceptor has accepted, its stored pair is unique.

Liveness

Proving liveness (that eventually a value will be chosen) is much harder because it requires fairness assumptions about the network and process scheduling. In Coq, we can prove bounded liveness under certain assumptions: if there is a distinguished proposer that is alive and can eventually contact a stable majority, and if messages are eventually delivered, then the proposer will succeed. The proof often uses a “eventual leader” argument. Many verification projects only prove safety, leaving liveness to informal reasoning or to a separate model checking pass.

5. Real-World Impact: How Formal Verification Saved (or Could Save) Systems

Formal verification of distributed protocols is not just academic. Several high-profile systems have been verified:

• IronFleet: Microsoft Research used Dafny to verify a Paxos-based system called IronFleet that combines a verified protocol with a verified OS kernel. They proved both safety and liveness.
• Verdi: The Verdi framework (University of Washington) provides a verified implementation of Raft (a consensus protocol alternative to Paxos). The Raft implementation in Verdi was proved to have the same safety guarantees as the specification.
• Amazon Web Services: AWS uses formal verification for its key-value store and its consensus layer. Their “networked system verification” team has used TLA+ for specification and model checking, and they are moving towards machine-checkable proofs.

These projects demonstrate that formal verification is feasible for real code. The overhead is high—writing the proof can take months—but the payoff is immense: the resulting system is provably bug-free for the verified properties.

For the nuclear reactor analogy, consider a system like the one that controls the cooling pumps in a reactor. If the consensus protocol that decides which pump to activate has a subtle bug, the result could be catastrophic. Formal verification could be the difference between a graceful shutdown and a meltdown.

6. The Future: Proofs as a Standard Practice

The barrier to entry for formal verification is lowering. Tools like Coq, Isabelle, and Lean are becoming more user-friendly. Libraries like Verdi and Disel (Distributed Separation Logic) abstract away much of the boilerplate. For distributed systems engineers, the skill of writing proofs is becoming as valuable as writing tests.

We are also seeing the emergence of “proof engineering” as a discipline. Companies like Galois, Inc. and groups like the MIT PDOS lab are creating verified systems software. The day may not be far off when every major protocol (Paxos, Raft, PBFT) comes with a verified Coq proof as part of its documentation, similar to how cryptographic protocols come with security proofs.

The nuclear reactor control system should not just be tested; it should be proved correct. Consensus protocols are the nuclear reactors of the data center. They deserve the same rigor.

7. Conclusion: From Nuclear Reactors to Distributed Databases

We began with a nuclear reactor control system. We end with a distributed database. The analogy holds because both require absolute certainty about a single, critical property: that the system will not diverge into contradiction.

Paxos is elegant, but elegance does not guarantee correctness. Informal proofs are prone to oversight. Formal verification with Coq provides a way to build an airtight case for safety and liveness. It forces us to examine every edge case, every interleaving, every crash scenario. It replaces intuition with mathematics.

The next time you send a message, buy a stock, or search Google, remember that a consensus protocol is running. And if that protocol has been formally verified, you can sleep a little better, knowing that the juggling chainsaw is being handled by a machine that never drops it.

(Word count: ~10500 including the intro and all sections. Code snippets are illustrative.)