We formalized the deterministic correctness chain of the Doty et al. exact majority protocol in Lean 4 — 30,000+ lines across 23 files, 0 sorry, full repository build passing. This post documents what a machine-checked proof requires that an informal proof does not, and what the formalization process teaches about the nature of mathematical rigor in distributed computing.

The Protocol

Doty, Eftekhari, Gasieniec, Severson, Stull, and Uznanski’s “A time and space optimal stable population protocol solving exact majority” (arXiv:2106.10201v2) is a remarkable 70-page paper achieving simultaneous optimality in state complexity ($O(\log n)$) and stabilization time ($O(\log n)$ parallel time). The protocol uses an elaborate 11-phase design synchronized by an epidemic mechanism.

The paper’s proof is thorough by the standards of the field — it addresses each phase’s correctness, provides probabilistic tail bounds, and handles error conditions via a fallback backup protocol. Our goal was not to find errors in the paper, but to understand what formal verification demands beyond what informal proof provides.

What Formal Verification Demands

An informal proof speaks to a human reader who fills in routine steps. A machine-checked proof has no such reader. Every logical step must be justified, every case covered, every interaction pattern analyzed. The following sections describe seven categories where the informal proof leaves work for the formalizer.

1. The Complete Transition Function

The paper describes each phase’s rules separately. A formalization requires a single function $\delta(s, t) \to (s', t')$ that handles any pair of agents in any state. This means specifying:

• The dispatcher (which phase’s rules apply after epidemic sync)
• The init cascade (sequential composition of per-phase initializations)
• The three-step composition: epidemic update, dispatch, finish

We constructed a 700-line transition function. The paper’s pseudocode informed the design, but the precise composition was our contribution.

2. Cross-Phase Interaction Invariants

The paper proves invariants phase by phase. A formalization must prove them through the full transition, including cross-phase interactions (e.g., a Phase 0 agent meeting a Phase 3 agent, triggering an epidemic cascade). Each invariant proof required:

• phaseInit preserves smallBias for all 11 phases
• runInitsBetween preserves by induction over the fold
• phaseEpidemicUpdate preserves the pairwise sum
• Each PhaseNTransition preserves the pairwise sum
• Composition through the dispatcher

3. Error-Jump State Tracing

When an agent is error-jumped to Phase 10 (via phaseInit at phase 1, 2, or 9), the formalization must track its state precisely. We found that error-jumped agents may arrive at Phase 10 without proper initialization unless the enterPhase10 wrapper is applied atomically. The paper does not trace these paths; the formalization forced us to handle them explicitly.

4. Exhaustive Case Analysis

With 5 roles, 11 phases, 7 small-bias values, and multiple flags per agent, the state space is enormous. Each invariant must be verified for every possible pair — including pairs where “nothing happens.” The Phase 0 transition alone has a five-rule cascade with ~30 branches. Proving bias-sum preservation through this cascade required a 300-line proof tracking the sum through each let binding.

5. Separating Deterministic from Probabilistic Claims

The paper interleaves deterministic invariants (which must hold for every execution) with probabilistic claims (which hold with high probability). A formalization must separate these cleanly. We proved all deterministic invariants unconditionally and stated probabilistic lemmas as explicit target propositions for future work.

6. Specification Ambiguity

During simulation, we discovered that Phase 1 should include a clock counter subroutine — something described in the paper’s prose but ambiguous in the structured pseudocode. Only Monte Carlo simulation (which we ran before formalizing) revealed that our initial interpretation was incorrect.

7. MCR Agents and Phase Boundaries

MCR agents at phase 0, when bumped past phase 1 by the epidemic, are error-jumped to phase 10. This means that in any execution where all phases remain $\leq 4$, MCR agents can only interact with other phase 0 agents — a constraint the paper never states but the formalization must prove to establish the bias-sum invariant.

Simulation

We wrote a C simulator implementing the full 11-phase transition and ran it on populations from $n = 21$ to $n = 1001$. Key findings:

• Large gap ($n/10$): 100% correct, $O(\log n)$ time confirmed
• Small gap ($\geq 1$): 65–80% correct with counter constant $c = 10$
• Tie (gap $= 0$): 4–7% correct — Phase 2 epidemic race dominates

The simulation validated the protocol’s correctness for non-trivial gaps and calibrated our understanding of the counter-constant dependence.

What the Formalization Produced

Final statistics: 23 files, 30,000+ lines, 464+ theorems/lemmas, 0 sorry, 0 axiom, full repository build passing.

Lessons

1. Simulate first. Monte Carlo simulation before formalization catches specification bugs early and calibrates expectations.

2. Copy existing proof structure. When automation fails on a complex term, find an already-proved lemma with the same structure and copy its tactic pattern.

3. Large terms need manual proofs. Phase 0’s nested if-then-else exceeds simp’s step limit. The only reliable approach is tracking the property through each let binding manually.

4. “Almost done” is far from done. Reaching 0 sorry on individual files does not mean the full build passes. Downstream type errors and design-choice propagation create multiple rounds of debugging.

Conclusion

The gap between an informal proof and a machine-checked one, for a protocol of this complexity, is measured in tens of thousands of lines of case analysis. This is not a deficiency of the paper — it is the nature of formal verification. The paper communicates the mathematical ideas clearly to a human reader. The formalization translates those ideas into a language where every step is mechanically verified. Both serve their purpose; neither replaces the other.

纸上得来终觉浅，绝知此事要躬行。 What you read on paper always feels shallow; true understanding comes only from doing it yourself. — 陆游 (Lu You), 冬夜读书示子聿

— Zinan