The Case for Verified Consensus

Distributed systems have leaned on consensus for decades — databases replicate for durability, cloud platforms fail over across regions, and every one of them settles disagreements through some protocol most users never see or think about. Blockchains inherit that same problem under harsher constraints: no operator holds root access to break a tie, no snapshot exists to roll back to, and the thing being agreed on is frequently somebody else's money. That's what makes consensus correctness the actual product rather than an implementation detail — get it right and a ledger earns trust without needing to trust any single party; get it wrong, and every guarantee built on top of it, finality, custody, cross-chain settlement, stops meaning anything the instant two honest nodes disagree.

Every so often a claim arrives confident enough to deserve a check of its own. The claim at the center of this post is that formal verification — specifically the Lean 4 theorem prover combined with Rust-to-Lean transpilation pipelines and AI-orchestrated proof search — has crossed the threshold from research toy to production requirement over roughly the last fifteen months, succeeding precisely where dynamic testing is supposed to top out.

The stakes named are specific, not abstract. A permissionless network has no trusted operator standing by to reboot the cluster or reconcile from a backup when nodes disagree — the same consensus mechanism that decides which transactions are real is also the last line of defense between an attacker and someone else's money, with no maintenance window if it fails. That's exactly why sequencer engines, L1 consensus layers, and cross-chain bridges get named as case studies, backed by ten references, building toward the claim that machine-checked "zero-sorry" proofs are becoming the industry's baseline expectation.

The workhorse that Lean 4 provides is real.

That's why Lean 4 can treat a proof as a checkable artifact at all: the kernel type-checks a proof term exactly the way a compiler type-checks a program, because as far as the kernel is concerned those are the same act. Aeneas and Charon extend that same trust one step further, translating Rust into exactly the form the kernel can check — real tools, built by real people, to solve a real problem. But an argument whose entire thesis is "don't trust an unverified claim, verify it" is making a promise about its own footnotes too — and that promise starts to wobble with a decade-old "settled" proof that, in 2019, turned out not to be.

01 The Cost of Getting Consensus Wrong

Three pieces of framing set up the cost argument: (1) how consensus correctness used to be established before machine-checked proof, (2) what getting it wrong has actually cost, and (3) how production defends itself today.

Background: How Consensus Correctness Used to Be Established

Distributed consensus has always had a validation problem. The question of how mutually distrusting parties agree on a single shared fact has mattered since the 1970s and '80s for a life-or-death reason, not an academic one: SRI's SIFT project needed redundant flight-control computers to reach the same decision even when one of them was feeding the others corrupted or contradictory data, the exact scenario Lamport et al. formalized as the Byzantine Generals Problem, because a single malfunctioning sensor on an aircraft can't be allowed to talk the rest of the system into a fatal disagreement.

Consensus papers responded to that stake by making a hand-written correctness argument part of the deliverable, not an afterthought — and that convention, not machine-checked proof, is what the field settled into for the next four decades:

• Lamport's own Paxos ("The Part-Time Parliament," 1998) set the template: state the protocol, state the invariant, argue by hand that the invariant holds inductively, and let peer review — not a proof assistant — be the correctness gate.
• Castro and Liskov's PBFT (2002) followed the same pattern: Section 4.5 sketches a safety argument resting on quorum intersection among 2f+1-sized "prepared" certificates over 3f+1 replicas, then defers the full proof to a companion technical report — hand-written, formalized with I/O automata rather than TLA+, and never machine-checked.
• Ongaro and Ousterhout's Raft (2014) did too, with its safety argument in the appendix of Ongaro's Stanford dissertation — a hand-written proof accompanying a TLA+ specification used for precision, not automated verification.

TLA+ recurs throughout that list, so it's worth pausing on what it actually is. First proposed by Lamport (2002), TLA+ is a formal language specifically designed to describe and verify system behavior. It combines first-order logic, set theory, and temporal logic, representing system behavior as a sequence of states in which an initial state, transition conditions, and system properties together describe an execution path. The approach is relatively concise and supports decomposing and modularizing large specifications — including the asynchronous distributed systems every protocol on this page is one of.

The gap between that and a full machine-checked proof isn't exactly small. A later project, Verdi, fully mechanized Raft's safety property in Coq in 2015 — the first mechanically-checked linearizability proof for the algorithm — and it took roughly 50,000 lines of proof script, for one already-understood, already-battle-tested protocol.

That cost, not a lack of tooling, is the real reason pen-and-paper proofs became the discipline's default: interactive theorem proving existed the whole time, but formalizing a full distributed protocol was — and often still is — a project of its own, disproportionate to what a conference deadline allows.

The hand-written era's own track record is checkered, and the canonical case is EPaxos: a widely-cited protocol whose decade-old hand-written proof turned out to hide a real safety violation, found only once someone went looking for it in earnest. Peer review had been the correctness gate, and it had been wrong; that story is told in full two sections down, and its machine-checked-era counterpart alongside it.

For two decades the industry's answer was dynamic testing: unit tests, property-based fuzzing, and Kyle Kingsbury's Jepsen suite — a fault-injection framework that deliberately partitions networks, kills nodes, and skews clocks to see whether a database really delivers the consistency it advertises. Jepsen spent a decade finding split-brain conditions and data loss in MongoDB, Cassandra, CockroachDB, and Elasticsearch — systems that had already passed thousands of deterministic tests. Jepsen is real, its track record is real, and the conclusion it points to is correct: testing samples a space; it doesn't cover it.

Figure 1 lays out that whole spectrum, testing through formal proof — and the Lean 4 end of it is already the bleeding edge in practice, not just in theory, as the Mysticeti formalization later in this post makes concrete.

Flawed Consensus

Actual consensus bugs — the kind that live in the protocol layer itself, not in a smart contract sitting on top of it — have mostly been quieter but no less real: Tendermint-based Cosmos chains have stalled on voting-power edge cases and epoch-boundary mismatches, and Solana has taken multi-hour outages from resource-exhaustion and clock-drift conditions in its leader schedule. Layer-2 sequencers have shipped their own version of the same story more than once: Arbitrum's Sequencer got stuck after a burst of transactions in September 2021, stalled again under an Ethscriptions-driven batch-posting backlog in December 2023, and Base halted block production twice in one week in June 2026 after a stale-journal-state bug produced a receipts root validators correctly rejected.

A validator set can't roll back a finalized block without a hard fork, and a hard fork is a political event, not a technical one.

The dramatic ones — the bugs that actually split a network or forced a chain to reorganize — are fewer, older, and much better documented:

• In August 2010, an integer overflow in Bitcoin's transaction-validation code let a single block mint 184,467,440,737 BTC — nearly 9,000 times the intended 21 million cap — and undoing it required a coordinated ~53-block reorganization of the chain (the value overflow incident, CVE-2010-5139).
• In March 2013, a database-layer mismatch between Bitcoin 0.8.0 and its predecessors split the network in two — most of the network's hashing power sat on a chain the rest rejected — until the largest miners downgraded to 0.7, orphaning roughly 24 blocks and letting a real double spend through in the meantime (BIP-50).
• In November 2020, a consensus bug in Geth — then running roughly 80% of the Ethereum network — let a single transaction split the chain at block 11234873 for about two hours, knocking Infura and much of DeFi offline and halting ETH trading on major exchanges, in what developers called the network's most serious incident since the DAO (CVE-2020-26241).

None of the three needed a flawed spec or a broken incentive design to be expensive — they were plain implementation bugs in consensus-critical code.

Their cost shows up differently from headline thefts: forced reorgs, split networks, and halted services rather than drained wallets — exactly the class of bug machine-checked verification exists to catch.

How Production Consensus Actually Gets Tested

None of the machinery described so far — Lean 4 proofs, AI-orchestrated tactic generation — is how Ethereum or Solana actually defend against the bugs described above, today, in production. Both networks lean on client diversity instead (see a forthcoming blog post): multiple, independently-written implementations of the same protocol, run in parallel, precisely because a single codebase — however carefully audited — shares one blind spot across every validator running it.

• Ethereum's execution layer runs Geth, Nethermind, Besu, and others; its consensus layer runs Lighthouse, Prysm, Nimbus, Teku, and more, with the community actively tracking and discouraging any single client from crossing roughly a third of the network, since a bug in a dominant client can finalize an invalid chain outright.
• Solana ran on one dominant client, Agave, for years; Firedancer — an independent, from-scratch reimplementation in C by Jump Crypto — only reached mainnet in 2026, giving Solana real client diversity for the first time just as it heads into its Alpenglow consensus upgrade.

The mechanism holding these independent implementations to identical behavior isn't a Lean 4 kernel — it's Hive, Ethereum's cross-client end-to-end test harness. Hive boots a simulated network from real client images — Geth, Nethermind, and Besu on the execution side, Lighthouse, Prysm, and Teku on the consensus side — and runs scenarios a unit test can't stage. A staple: make one node propose a block with a corrupted state root, then verify every other client rejects it and the network keeps finalizing the valid chain — precisely the failure mode a dominant-client bug produces, and the one the Nethermind incident later in this section actually hit.

On top of that sits a shared conformance suite derived directly from the protocol spec, covering epoch processing, fork-choice, validator shuffling, reward calculation, SSZ serialization, and more, versioned per hard fork from Phase0 through the upcoming Fulu and Gloas — plus devnets and shadow forks that replay real mainnet state to stress-test upgrades before they ship.

The suite runs the same test logic under two parameter presets, because a conformance failure can hide in either. The mainnet configuration uses the production constants — 12-second slots, full epoch lengths, a validator set in the hundreds of thousands — so a passing test means the code handles real mainnet parameters. The minimal configuration scales every parameter down — a handful of validators, shorter epochs — so the same tests run in seconds in CI and on devnets. The two columns below count the test vectors each configuration produced, per hard fork:

Not Hypothetical

That mechanism — a deviating client exposed and contained by disagreeing with the majority — isn't hypothetical. In January 2024, a bug in versions 1.23–1.25 of the Nethermind execution client caused roughly 8% of Ethereum's validators to start producing invalid blocks. Because Nethermind was one of several independent execution clients rather than the only one, the network as a whole kept finalizing correctly on the majority behavior — the bug was contained to the validators running that specific client, visible almost immediately as a minority disagreeing with everyone else, and patched within hours. A Geth-scale bug in a network with only one dominant client wouldn't have that containment property at all.

The Nethermind incident wasn't the first time this mechanism did its job — the earlier case is the more dramatic one, and it's the reason Ethereum takes client diversity as seriously as it does. In August 2020, Prysm ran over 65% of the nodes on the Medalla public testnet when a Cloudflare clock-sync bug knocked it offline, triggering more than 3,000 slashing events and collapsing network participation from roughly 75% to the single digits within hours — a client-concentration failure playing out exactly as feared, months before mainnet and with no real stake at risk. Prysmatic Labs' own postmortem, days later, was unusually blunt about what that timing meant:

It would have been really terrifying if the Medalla public testnet ran uninterrupted, with perfect performance right before mainnet, and then this bug occurred with real money at stake once eth2 launched. [...] This was the best thing to happen to a testnet.

Solana is the network that counterfactual describes: its validator fleet ran almost entirely on one client, Agave, until Firedancer's mainnet arrival in 2026 — and in December 2025, Anza, Agave's maintainer, privately disclosed two critical bugs in it. Malicious gossip messages could crash validators outright, and a flood of unverified vote messages could stall consensus; both were patched in the urgent v3.0.14 release of January 2026, coordinated with Firedancer, Jito, and the Solana Foundation. A day after the patch shipped, only 18% of stake had upgraded — the network's "always-on" promise was still running on software that a coordinated attacker could have stalled. Nothing was exploited; the exposure window is the point.

02 What “Correct” Actually Means

Before grading the remedy, the yardsticks it's graded against. Every consensus protocol specification rests on two properties Leslie Lamport formalized in the 1970s: safety ("nothing bad happens") and liveness ("something good eventually happens").

Safety for a consensus protocol unpacks into agreement — no two honest nodes decide differently for the same slot — validity — a decided value must trace back to a legitimate proposal — and integrity — no node decides twice. Liveness unpacks into termination — every honest node eventually decides — and progress — the network keeps committing blocks despite bounded adversarial behavior.

One more piece of framing before the verification tooling: the CAP theorem, which sits one level up from safety and liveness rather than inside them. Eric Brewer's conjecture, proven by Gilbert and Lynch in 2002, says a distributed system can't simultaneously deliver consistency, availability, and partition tolerance — not a free pick-any-two: during a partition it's a hard choice between consistency (all nodes see the same data — a safety property) and availability (every request gets a response — a liveness property).

Public blockchains sit at the extreme consistency-over-availability end, stopping finalization when the network splits rather than risking two histories — which is why safety and liveness, not CAP, are what consensus proofs actually pin down, and why CAP rarely shows up in formal verification papers. Two families of tools exist to pin them down.

Model Checkers

Model checkers like TLA+'s TLC, SPIN, and UPPAAL can verify safety and liveness automatically for small, abstract protocol sketches — three or four nodes, a handful of rounds — but they run into the state space explosion problem almost immediately past that.

Add nodes, rounds, or message types and the reachable state graph grows combinatorially; a protocol that allows k distinct message types across n nodes with a buffer of size m has a state space on the order of ∏_i |S_i| × (m!)^k, and no amount of clever traversal changes the fact that it's finite for any one instance, but unbounded across instances — a different problem than the "arbitrary n" guarantee a real deployment needs — a limitation Feng and Zhang's 2026 survey of the broader consensus-verification landscape traces across model checkers generally, not just this one case.

Theorem Provers

Interactive theorem proving sidesteps the explosion by proving a universally-quantified statement directly rather than enumerating states: instead of checking that a 4-node instance doesn't violate safety, you prove that no instance, at any n, does.

The standard technique is the inductive invariant: a predicate I(S) over global states, discharged through three proof obligations — (1) a base case (I holds at the initial state), (2) an inductive step (if I(S) holds and a valid transition produces S′, then I(S′) holds too), and (3) entailment (I(S) implies the actual safety property you care about).

Establishing one is genuinely hard, because local per-node facts — "node i has locked block B at round r" — have to compose into global facts across the whole quorum structure, such as the standard BFT quorum-intersection lemma: any two quorums of size ⌈(2n+1)/3⌉ share at least one honest node. The quorum-intersection proof coming up next discharges that exact obligation end-to-end, in working Lean 4 rather than in prose.

03 Formal Methods Are Not a Panacea

The cost side is only half of the argument. That consensus bugs are expensive motivates the search for a remedy, but says nothing about whether the remedy on offer — machine-checked proof — can itself be trusted. The other half is that remedy's track record: published proofs, treated as settled, that later turned out to be wrong — a history that belongs next to the production incidents above, not treated as a separate story.

The remedy fails in four distinct ways, each striking a different point in the chain. (1) A proof can be simply wrong — it doesn't establish what it claims, and the protocol carries an undiscovered bug for years, as with EPaxos. (2) It can be right but unshipped — it finds a genuine bug in deployed code, then the fix stalls before the network adopts it, as with Mysticeti. (3) It can be partial — it covers a simplified or abstract model, not the implementation that actually runs, as with the HotStuff formalizations. (4) It can be narrow — it certifies the algorithm in isolation, not the composed system a validator runs in production, as with Tendermint. The four cases that follow are one of each.

Wrong, unshipped, partial, narrow — the four failure modes above read as four different stories, but they're failures against the same two yardsticks: safety and liveness. However different their proximate cause — a flawed proof, a stalled patch, an abstracted model, an isolated algorithm — each one ultimately means a validator can either disagree with an honest peer or simply stop making progress, the same two outcomes this post keeps returning to.

Wrong Proof, Undetected Bug

EPaxos, a widely-cited Paxos variant published at SOSP 2013 with an accompanying TLA+ specification and a hand-written safety proof, was treated as settled for the better part of a decade. In 2019, Pierre Sutra found and published a genuine safety violation in both the specification and the reference implementation: under a specific interleaving, replicas could disagree about a command's dependencies — breaking the exact property the original proof claimed to establish. One of EPaxos's own authors later acknowledged the team never got around to formalizing the protocol's recovery path, which is precisely where the bug lived.

Ryabinin et al.'s follow-up paper, presented at OPODIS 2025, was still fixing and simplifying the protocol twelve years after its original publication; its authors' verdict on the original is matter-of-fact — "the protocol is very complex, ambiguously specified and suffers from nontrivial bugs." A hand-written proof and a bounded TLA+ model check are real evidence — they are not the same claim as a machine-checked proof that holds for arbitrary n, and EPaxos is the textbook case for why that gap matters.

Right Proof, Unshipped Fix

The same pattern is playing out right now on a live network, not a decade-old protocol. Qiu et al. built machine-checked safety and liveness proofs for Sui's Mysticeti consensus protocol in the Rocq proof assistant, presented at IEEE S&P 2026 — and their test case against the actual deployed implementation found it incorrect, in a way that can lead to real liveness attacks.

The bug is a specific one: Sui's implementation lets an honest node "jump" over a round without creating a vertex there, and the paper constructs an explicit infinite trace, under that behavior, where no leader vertex is ever committed. The authors audited the actual Sui source (commit 2f52a72) and confirmed it matches the vulnerable behavior, then proved a fix — a restriction on which rounds a node is allowed to jump over, backward-compatible with nodes that haven't upgraded — and mechanically verified that the fixed version restores liveness.

As of publication, that fix was proposed and proven, not yet shipped: Qiu et al. state plainly that "we have contacted Mysten Labs and they have acknowledged the issue. We are currently working with them to resolve the liveness issues." A check of the public Sui and IOTA repositories as of this writing finds no implementation of the round-jump restriction — the only round-jump-adjacent change in either project is an unrelated IOTA threshold-clock quirk fix, and Sui's consensus code has evolved considerably since the audited commit without touching the vulnerable behavior.

IOTA, whose chain forks Sui's Mysticeti implementation, is reportedly pursuing a different fix of its own: Qiu et al.'s own related-work section points to Polyanskii, Mueller, and Vorobyev's Starfish paper, which proposes requiring every honest process to create a vertex in every round — a stricter rule than Qiu et al.'s fix, and one Starfish requires from the start of protocol execution rather than allowing mid-run adoption. A proof that catches a real bug is exactly what this technology is supposed to do — but catching it and shipping the fix are two different milestones, and only the first one has happened so far.

Proven Model, Unproven Code

Aptos, whose AptosBFT is itself a HotStuff descendant, hasn't had a proof at that level tied to its actual deployed implementation — the formal-verification effort specific to Aptos has gone almost entirely into the Move VM and framework, not the BFT protocol underneath it. Two major, currently-running networks, two very different amounts of scrutiny on the part that actually orders transactions.

HotStuff itself — the protocol underlying both AptosBFT and Diem/Libra's DiemBFT — has drawn more mechanized attention than any single deployment built on it. Jehl, at FORTE 2021, proved safety of a simplified HotStuff using Ivy and the TLA+ Proof System, showing along the way that HotStuff's tree-shaped commit structure — a real departure from the view-by-view model older BFT protocols use — makes the verification problem harder than that older model does. Carr et al. published a machine-checked Agda safety proof of an abstract HotStuff/LibraBFT model at NFM 2022, and, independently, Kukharenko et al. specified and model-checked HotStuff in TLA+/TLC in 2021 for an unrelated industrial ledger project.

None of the three closes the gap Mysticeti's proof did: Jehl's and the Agda proof both cover safety on a simplified or abstract model with no tie to concrete implementation code, and TLC-style model checking runs into the same state-space-explosion ceiling as any other bounded checker — it doesn't hold for arbitrary n.

HotStuff the protocol has been formalized more than once; HotStuff as actually deployed inside Aptos hasn't.

Proven Algorithm, Unproven System

Tendermint tells an even more interesting version of this story, because the naïve framing — battle-tested, never formally proven — turns out to be wrong. Tendermint, now maintained as CometBFT, settles blocks for well over a hundred chains in the Cosmos ecosystem, Celestia, dYdX, Injective, Osmosis, and Kava among them, and that scale is real production exposure, not a marketing number.

It also has a real proof: in 2021, Galois and Informal Systems independently verified Tendermint's core safety property — that two well-behaved nodes never disagree, given standard quorum-intersection assumptions — plus two accountable-safety properties, that misbehaving validators are identifiable and honest ones can't be framed, using two different toolchains, Ivy and TLA+/Apalache, that reached the same conclusions. The proof itself is compact: the protocol description runs about 350 lines, the Ivy proof of it only 125.

That adoption predates the proof, though, and isn't downstream of it. Cosmos Hub's mainnet launched in March 2019; the SDK-driven app-chain ecosystem grew from there on developer ergonomics and IBC interoperability, which itself only shipped in 2021 — the same year as the Galois/Informal Systems proof, not before it. Nobody picked Tendermint because it had been proven correct; the proof arrived after the adoption case had already been made on other grounds entirely.

Two things complicate the reassurance. An earlier formalization effort, Amoussou-Guenou et al.'s "Dissecting Tendermint" (2019), found real bugs in preliminary versions of the protocol during the process of formalizing it across different network and adversary models — the same EPaxos-shaped lesson that writing the formal model down is itself how some of these bugs surface.

A 2025 paper on Tendermint's termination properties states plainly that prior safety and termination analysis — the 2021 proof included — "has been done in a standalone fashion, with no consideration of the composition with other protocols" it actually runs alongside. The 2021 proof is real and it holds for the algorithm as specified; it still doesn't cover the composed system a validator actually runs, which is the same refinement-proof boundary this post keeps circling back to, one level up.

The production record doesn't contradict any of this. The most visible recent Tendermint-ecosystem chain halt — Cosmos Hub, June 5, 2024 — traces to a bug in the Cosmos SDK's staking and interchain-security modules, not the CometBFT consensus algorithm: adding one validator and removing another in the same block briefly pushed a validator-power index past its configured cap. That's a real production failure sitting in the layer around consensus, not the safety property the 2021 proof actually covers — which cuts both ways: either a point in Tendermint's favor, or a demonstration of just how narrow "the consensus algorithm is proven safe" turns out to be once the composed system a validator actually runs is what's in question.

The Gap No Refinement Proof Closes

Even setting the four cases above aside, there's a more structural issue with the whole thesis: a proof only ever certifies conformance to a spec, and nothing in the machine-checking toolchain — not the prover's kernel, not the extractor, not a zero-sorry refinement proof — checks whether the spec itself says what the protocol designer meant it to say.

Follow the pipeline to its end and the same conclusion falls out. The Rust becomes a model; the model is refined against a spec; the refinement is proven; the certificate is issued. None of that machinery ever examines the spec itself — the hand-written statement of what the protocol is supposed to guarantee. An inductive invariant that's subtly too weak, or a quorum-size threshold that's off by a rounding error, will sail through the entire pipeline: the extractor will translate it faithfully, the refinement proof will succeed, and the zero-sorry certificate will be genuine.

The bug just moves up one layer, from "the Rust doesn't match the spec" to "the spec doesn't match reality" — which is precisely the distinction the software-engineering literature calls verification versus validation: verification asks "did we build the thing right," validation asks "did we build the right thing," and formal methods have always been much better at the former than the latter — the same point Carrone put succinctly: a proof is only as good as its spec.

The four cases above are each an instance of that boundary doing real work — a decision about the spec's scope, not a fault in the proof machinery. EPaxos's bug lived in the recovery path its authors never got around to formalizing, outside the spec entirely. Mysticeti's round-jumping behavior wasn't excluded by the original model until Qiu et al. added the restriction — a boundary the spec drew in the wrong place, not a broken proof of the model it did cover. HotStuff's formalizations prove the abstract algorithm, not the Rust or Go a validator actually runs — a boundary between model and code, not between correct and incorrect reasoning. And Tendermint's 2021 proof covers the standalone algorithm, not the composed system running alongside the mempool and state-sync plumbing wired around it. Even a perfect pipeline leaves that boundary exactly where the designer put it.

This isn't a hypothetical concern specific to consensus — it's the same lesson that applies to AI-generated code more broadly: test suites and even formal specs are only as good as the invariants someone thought to write down, and stubbornly under-specified systems pass every check you thought to run right up until the one you didn't.

04 Lean 4: A Real Paradigm Shift in Interactive Proving

Interactive theorem proving isn't new — Coq and Isabelle/HOL have both existed since the 1980s, and both have real pedigree: Coq underlies CompCert, a verified C compiler, and Isabelle/HOL underlies seL4, a verified microkernel. What's newer is Lean 4, developed initially at Microsoft Research under Leonardo de Moura and now maintained by the Lean Focused Research Organization (Lean FRO).

That timeline covers the tools; it says nothing about what they've actually verified. Feng and Zhang's 2026 survey catalogs the theorem-proving landmarks by target protocol, property proved, and toolchain — a useful reality check on the field's actual track record before this post narrows in on Lean 4 specifically:

That highlighted row is worth flagging before moving on: the Jolteon proof, built on Qiu et al.'s own LiDO framework in Coq, is the direct predecessor of the same authors' later LiDO-DAG proof of Mysticeti in Rocq — Coq's 2024 rename — the “right proof, unshipped fix” case study earlier in this post. It's one of the few entries in this survey where a single theorem-proving lineage tracks a protocol all the way from a research prototype to something actually running in production.

Lean 4 is grounded in the Calculus of Inductive Constructions (CIC), the same dependent-type-theory family Coq uses, but it made a specific set of engineering bets legacy provers didn't: a single unified language for specifications, tactics, and the macro system itself (rather than Coq's split between Gallina, Ltac, and OCaml build tooling), compilation to fast native C code rather than interpretation, and a metaprogramming layer that makes writing custom tactics and SMT bindings (Z3, CVC5) a first-class activity rather than a research project of its own.

Stack those three engineering bets up against the field it's displacing and the gap is concrete, not just rhetorical:

Safety Proofs

What a Lean 4 safety proof actually looks like, stripped to its skeleton, is a function signature whose body is the proof — this snippet is close to how it was originally written, sorry included, not rewritten for this post:

theorem consensus_safety
    (n f : Nat)
    (h_byz : f < n / 3)
    (trace : ExecutionTrace n)
    (h_valid : ValidTrace trace) :
    NoDoubleSign trace := by
  -- proof steps constructed via the Lean 4 tactic engine
  sorry

Everything after by is tactic script — the part an engineer (or, increasingly, an AI tactic generator — more on that below) has to fill in. The sorry above is the honest state of an unfinished proof; it compiles, and it proves nothing. Consensus protocols get formalized as inductive operational semantics — messages, per-node state, and a global transition relation — which is what makes properties like quorum intersection statable and provable in the first place. This scaffold, again, is close to how it was originally written:

-- inductive definition of consensus network messages
inductive Message (V : Type) where
  | proposal (round : Nat) (value : V) (sig : Signature)
  | vote     (round : Nat) (blockHash : Hash) (nodeId : Nat) (sig : Signature)
  | commit   (round : Nat) (blockHash : Hash) (sig : Signature)

-- local node state representation
structure NodeState (V : Type) where
  nodeId        : Nat
  currentRound  : Nat
  lockedValue   : Option V
  validValue    : Option V
  votesReceived : List (Message V)

-- global network transition
inductive Step (V : Type) : GlobalState V → GlobalState V → Prop where
  | receiveVote (s : GlobalState V) (m : Message V) :
      ValidMessage s m → Step V s (ApplyMessage s m)
  | timeoutRound (s : GlobalState V) (nodeId : Nat) :
      Step V s (AdvanceRound s nodeId)

Formalizing in Lean

Unlike the sorry-containing skeleton above, this one actually closes, written for this post, specifically for this comparison — not lifted from anywhere — and it's been through a real toolchain: the file below type-checks against Lean 4.32.2 and Mathlib as of this writing, with no sorry and no admitted step.

import Mathlib

variable (Node : Type) [DecidableEq Node]

-- Pigeonhole: two quorums this large can't both dodge every honest node.
theorem quorum_intersection_has_honest
    (n f : Nat) (h_byz : 3 * f < n)
    (faulty q₁ q₂ : Finset Node) (h_faulty : faulty.card = f)
    (h_q₁ : 2 * n + 1 ≤ 3 * q₁.card)
    (h_q₂ : 2 * n + 1 ≤ 3 * q₂.card)
    (h_bound : (q₁ ∪ q₂).card ≤ n) :
    ∃ node ∈ q₁ ∩ q₂, node ∉ faulty := by
  by_contra h_none
  push_neg at h_none
  have h_sub : q₁ ∩ q₂ ⊆ faulty := h_none
  have h_inter_le : (q₁ ∩ q₂).card ≤ f := h_faulty ◂ Finset.card_le_card h_sub
  have h_pigeonhole : q₁.card + q₂.card = (q₁ ∪ q₂).card + (q₁ ∩ q₂).card :=
    (Finset.card_union_add_card_inter q₁ q₂).symm
  -- h_q₁, h_q₂, h_bound, h_pigeonhole, h_inter_le together contradict h_byz
  omega

Every element of that signature is doing real work:

• n and f — the network size and fault bound, left free so the lemma quantifies over every n: the guarantee a model checker can't provide.
• h_byz — the <1/3-Byzantine assumption.
• h_faulty — pins the faulty set to exactly f nodes.
• h_q₁ and h_q₂ — the quorum-size floor.
• h_bound — caps how much of the network both quorums can span.

Feed every hypothesis in the signature into omega — Lean's decision procedure for linear arithmetic over integers — and, with n and f ranging freely, the pigeonhole contradiction falls out mechanically. No sorry, no hand-waving in the tactic script: this is what a "zero-sorry" proof of a nontrivial lemma is supposed to look like, and this one has actually been through the kernel.

The Zero-Sorry Standard

Once the proof compiles, a second discipline matters as much as the proof itself: the zero-sorry standard. In Lean 4, sorry is a keyword that lets you write a proof skeleton and defer a step — it type-checks, but it's an admitted gap, not a proof. A "verified" codebase that still contains sorry statements, unvetted custom axioms, or unaudited dynamic casts hasn't actually proven what it claims to. This part of the argument is exactly right, and it maps cleanly onto dependent type theory's Curry-Howard correspondence between propositions and types, proofs and programs:

05 Scaling up Lean Proofs

The quorum lemma above is written for this post — but it is not a toy. The same theorem, in almost the same words, sits at the heart of real Lean 4 formalizations of full consensus protocols.

Mysticeti Consensus

George Danezis, one of Mysticeti's designers, maintains lean-dag, a machine-checked model of the uncertified DAG consensus family Mysticeti belongs to — hand-written, like Qiu et al.'s Rocq model, not derived from Sui's actual Rust the way Aeneas and Charon derive Lean from Rust. The development runs to roughly 25,000 lines of Lean 4 over Mathlib: every principal result depends on exactly Lean's three standard axioms, and every definition gets exercised on concrete models by decide before anything is proved from it. Its accompanying report, "Eventual DAG Synchrony," is quite explicit about what is proved versus what is assumed. Its quorum-intersection theorem is the direct analogue of the one above — two quorums of at least |Validators| − f members share a block — and its liveness account is the round-by-round no-stall guarantee:

theorem exists_common_mem_of_quorums {s t : Finset BlockId} {n : ℕ}
    (hs : ∀ q ∈ s, q ∈ U.ids ∧ (U.block q).round = n)
    (ht : ∀ q ∈ t, q ∈ U.ids ∧ (U.block q).round = n)
    (hsq : (Fintype.card Validator - F.f) ≤ (creatorsOf U.block s).card)
    (htq : (Fintype.card Validator - F.f) ≤ (creatorsOf U.block t).card) :
    ∃ q, q ∈ s ∧ q ∈ t

theorem populatedOn (vp : ViewPace U T N)
    (hcard : (Fintype.card Validator - F.f) ≤ T.card) :
    ∀ n ≤ N, PopulatedOn U T n

The quorum arithmetic is the same n > 3f bound, written as quorums of at least |Validators| − f members, and the proof strategy is the same: peel off the faulty set, find a common honest creator, let omega finish. The report notes that quorum intersection is used exactly once, in the base case of the persistence argument — above that layer, height is carried by transitivity alone. The specification is also careful to count quorums on creators rather than on raw references: "a quorum of blocks from the previous round" means n − f distinct validators, the form every downstream proof actually wants.

What lean-dag models is Mysticeti-C itself: the first DAG-based Byzantine consensus to reach the three-message-round latency lower bound. It gets there by forgoing explicit certification — a block costs one broadcast, and a block two rounds above a leader acts as a certificate precisely when its references contain a quorum of blocks referencing that leader. Certification, in other words, is a pattern read out of the graph, not an artifact the protocol constructs, and the project's related-work survey maps the whole uncertified-DAG family — Hashgraph through Bluestreak — against exactly that distinction.

LeanDag/Mysticeti.lean is where the formalization cashes it out, targeting the commit rule itself: direct commit, direct skip, and the indirect rule that resolves undecided slots from later certificates. The paper's headline numbers (0.5s WAN commit latency at over 200,000 TPS, a 4× reduction on Sui) are measurements, not guarantees — the Lean proofs certify safety and liveness, not throughput.

The report is explicit about the shape of that liveness argument, and it is the same boundary this post keeps circling: safety assumes nothing whatsoever about the network — not even eventual delivery — and no liveness theorem mentions time.

The structural condition everything hangs on, eventual DAG synchrony, says only that beyond some round every correct block references every correct block of the round below:

def SynchronisedOn (U : BlockUniverse Validator BlockId Payload)
    (T : Finset Validator) (R : ℕ) : Prop :=
  ∀ n, R ≤ n → ∀ b ∈ U.ids, (U.block b).round = n + 1 →
    (U.block b).creator ∈ T →
    ∀ a ∈ U.ids, (U.block a).round = n →
      (U.block a).creator ∈ T → a ∈ (U.block b).refs

The report derives that condition rather than postulating it, from a single clause of view convergence (after stabilization, whatever one correct validator holds reaches every correct validator within Δ) plus build rules a protocol designer controls — derived, not assumed, which is the standard this post has been holding every case study to.

Living with the Proof

That derivation closes a loop with the Mysticeti bug from earlier in this post: the model's P8 clause excludes round-jumping outright — the behavior the Qiu et al. counterexample depends on — so lean-dag is not exposed to that flaw, and it can say why.

The repo's provenance note supplies exactly the disclosure this post has been asking for: the code and prose were co-written with heavy LLM assistance, the kernel machine-checks every theorem against its stated form, and whether the definitions capture their intended meaning has only human-plus-LLM review behind it. "Read critically," it says — and the repo's history agrees: 305 commits by one author in eleven days (August 3–13, 2026), a hundred files, ~25,000 lines of Lean 4, 238 of them co-authored by Claude and 213 with a Claude Code session link attached.

The kernel checked that every theorem holds exactly as written; whether those theorems were the right ones to write was still a call the humans, and the LLM working alongside them, had to make on their own.

This is what consensus formalization looks like when it targets a deployed protocol rather than a blog post. Igor Konnov, co-creator of the Apalache model checker used in the Tendermint proof above, keeps a parallel leanda — "Lean" plus "distributed algorithms" — whose machine-checked entries include agreement for single-shot Tendermint: two commits, roughly 8,600 lines of Lean in total, the agreement theorem itself just 137 of them — and, per the repo's own notes, generated from a Wunderspec model and following an existing TLAPS proof rather than formalized from scratch. The lemma above sits comfortably between the two.

With lean-dag it shares the very theorem — two quorums must intersect in a common block — and the proof style, right down to the omega that finishes the arithmetic. With leanda it shares the scale: one kernel-checked statement about one classic property, written to make a point rather than to cover a protocol. It is the same kind of mathematics at a fraction of the size — which is the point: the style is identical whether the target is a single lemma or a deployed protocol; only the labor and the stakes scale up.

AI-Aided Proof Dispatch

The most forward-looking claim on offer is that the historical bottleneck on formal verification — PhD-level formal-methods labor, measured in engineer-years per protocol — is dissolving under a neurosymbolic pairing of large language models and Lean 4's kernel.

The architecture is genuinely elegant, and it rests on a real asymmetry: LLMs are good at pattern-matching plausible next steps but hallucinate; Lean 4's kernel is a deterministic, from-first-principles type checker that cannot be talked into accepting an invalid proof step. Wire an LLM up as a tactic generator, let the kernel referee every proposed tactic, and you get a search loop where the model's creativity is unconstrained but its output is not — a false step gets rejected instantly, with structural feedback, and only a kernel-verified proof term ever counts as done.

LeanDojo and its baseline prover ReProver are real, publicly documented infrastructure for exactly this loop: they extract program-state trees and lemma databases from Lean source and expose them as a retrieval-augmented interface an AI agent can query — a legitimate and citable piece of the pipeline being described. It has quietly become the de facto foundation for the current generation of LLM provers, too: DeepSeek's Prover series, InternLM's step-prover, and ByteDance's BFS-Prover all build on it (BFS-Prover's model card cites "Mathlib, via LeanDojo" as its training-data source), and the MiniF2F and ProofNet benchmarks they all report against are LeanDojo's own Lean 4 datasets.

That extends into a Federated Formal Verification architecture: an AI orchestrator that routes sub-problems to whichever backend fits — arithmetic and bit-vector goals to SMT solvers, structural inductions to Lean 4, legacy proofs to Coq or Isabelle via cross-backend citation — and merges the results into one certificate.

The Isabelle leg of that picture isn't hypothetical: IsabeLLM (Jones & Knottenbelt, January 2026) wires DeepSeek R1 into Isabelle and uses it to verify Bitcoin's Proof-of-Work consensus, generating correct proofs for every nontrivial lemma in the verification — an independently checkable instance of exactly the legacy-prover-plus-LLM pattern described above.

The Uncited Productivity Numbers

The clearest real-world data point for "near-zero human labor," meanwhile, is missing from all of this entirely. Don Syme — creator of F# — published Lean Squad in April 2026: an agentic pipeline that produced over 1,200 machine-checked theorems across three codebases and caught a genuine bug in a drone autopilot along the way. It's a real, checkable result in exactly the direction gestured at by the uncited productivity figures below — nobody cites it.

All of this gets framed as a documented fifteen-month shift, mid-2025 to mid-2026, laid out as six paired claims:

The load-bearing empirical claims in that table — that AI-orchestrated provers now generate "over 70%" of routine proof tactics, that verification teams have shifted from 100% manual tactic-writing to mostly writing specifications — are exactly the kind of number that should come with a citation attached, and none of them do. Every row on the right is a plausible direction for the field to move in; none of them is a measurement — and the gap no refinement proof closes would remain even if every one of them were true.

06 From Proofs to Code

Here's the gap that made model checking and even the classic interactive-proving era less useful than they sound: proving an abstract TLA+ or Lean model correct says nothing about the Rust, Go, or C++ binary a validator node actually runs.

Implementation Divergence

Production consensus engines — CometBFT-rs, Reth, Solana Agave, ChonkyBFT — are systems code, and systems code has its own failure modes a protocol sketch never sees: integer overflow, use-after-move, async-runtime deadlocks under Tokio, deserialization panics on malformed input. A model can be flawless in TLA+ while its Rust implementation ships a bug the model never had a chance to catch.

This often gets called implementation divergence, and it's the correct name for a real problem.

That gap isn't evenly distributed across a small codebase, either.

The Size of the Gap

Real consensus modules run tens of thousands of lines, not a few hundred, and every one of those lines is another place implementation and spec can quietly part ways:

Algorand is the one system in that table with its own formal pedigree, and it's older than the fifteen months this post has been checking claims against: Alturki et al. built a machine-checked Coq model of its consensus protocol back in 2019. Following the same pattern as everywhere else in this post, that model was never tied to the 19,926-line Go implementation actually running above.

None of that code is exactly "padding."

The algorithm itself — the pseudocode in a HotStuff or Tendermint paper — fits comfortably in a few pages, because it treats an entire layer of production concerns as a single atomic primitive: "send message to node j" hides a transport stack built for an authenticated, adversarial network; "write to stable storage" hides a write-ahead log with fsync semantics, crash recovery, and corruption checks; "verify signature" hides quorum-certificate construction, BLS aggregation, and equivocation detection. Each of those is one line in the proof and thousands of lines in the codebase.

The bigger gap is the failure paths. Papers spend a page on the common case and a paragraph on recovery — leader election, view-change timeouts, reconciling state after a network partition heals.

From Rust to Lean: Aeneas and Charon

The proposed fix for that divergence problem is a transpilation pipeline built on two real, publicly available tools: Charon, an intermediate compiler frontend that hooks into rustc, resolves borrow-checker lifetimes, and lowers Rust's MIR into a clean intermediate format (LLBC — Low-Level Borrow Calculus); and Aeneas, which takes LLBC and translates Rust's imperative, mutable-reference style into pure functional Lean 4 code using what's called monadic state-passing: A Rust function that mutates &mut self and returns a Result becomes a pure Lean 4 function that takes the old state and returns a new one:

Once the extraction exists, the actual proof obligation is a refinement proof: show that every transition the extracted, low-level Rust code takes matches a transition the high-level, hand-written protocol spec would take, under some relation R connecting implementation states to spec states.

Below is the textbook shape of a refinement diagram — a commuting square, not a linear pipeline — and it's worth drawing that way, because the shape is the argument:

If that square commutes for every reachable state, any safety property already proven about the abstract spec transfers down to the actual binary a validator runs, for free.

This is a genuine advance over the TLA+-only era, and the tools behind it are real: Aeneas and Charon are real projects with real papers behind them, built specifically to close the implementation-divergence gap.

One of the areas to push back on is how far "refinement proof" actually reaches: refinement only guarantees the implementation matches the spec — and only as faithfully as the translation that connects them, since Charon and Aeneas sit inside the pipeline's trusted computing base, the same role the parser and elaborator play in Lean's own pipeline: no kernel checks them, so a bug in the extractor puts the divergence right back between the Rust and the model the proof is actually about. It says nothing about whether the spec was the right thing to prove in the first place.

From Rust to Proof, in Man-Hours

The 2022 Aeneas paper's own case study puts a real number on the labor question: proving a resizing hash table — insert, get, get_mut, remove, 201 lines of Rust without blanks or comments — functionally correct against a map specification took four person-days. Lean support was still listed as future work at the time, so this measures the pipeline's general shape rather than literally the Lean 4 case studies discussed elsewhere in this post, but it's the most concrete effort number in the tool's own literature.

The comparison points in that same paper matter more: a similar but simpler, non-resizing hash table took students three days to verify in VST, a Coq framework for C; the same kind of table took a week in CFML, working from higher-level OCaml; and a comparable map data structure took several weeks of full-time work in Low*, a C-targeting subset of F*.

None of those numbers are consensus-protocol scale, and none of them should be expected to scale linearly — proof difficulty tracks control-flow and state-space complexity, not line count. A naïve extrapolation from four person-days per 201 lines to Aptos's 63,156-line consensus module, roughly 300 times the size, lands around five person-years. That happens to sit close to the real, independently reported effort behind CompCert's much larger verified-compiler proof — six person-years, for 100,000 lines of Coq — and in the same range as Verdi's 50,000-line mechanized Raft proof from earlier.

Those tools' own repos back the estimate up, and reveal how concentrated the labor actually is.

• Aeneas, opened November 2021, has taken roughly 5,450 commits from 46 contributors to reach this point — but 80% of them, 4,353 commits, are Son Ho's alone, the same Son Ho who leads the paper cited above.
• Charon, opened two weeks earlier, shows the same shape in reverse: of its roughly 4,500 commits, 62% belong to a second Inria researcher, Nadrieril, with Ho contributing another 24%.
• Verdi's repo, open since November 2014 — almost twelve years — has taken about 1,300 commits, nearly two-thirds of them from its own two lead authors, James Wilcox and Doug Woos.

Person-years, not person-days, is the order of magnitude worth keeping in mind whenever a case study claims a production consensus engine got verified without saying how long it took.

Elusive End-to-End Guarantees

The second half is the hard one, and exactly one effort in this post has earned it. Qiu et al.'s Mysticeti verification — the "right proof, unshipped fix" story from earlier — proved the protocol's safety and liveness in the Rocq proof assistant, then did the part that makes a proof end-to-end: audited Sui's actual deployed source at 2f52a72, constructed an explicit infinite trace in which, under the implementation's round-jumping behavior, no leader is ever committed, and mechanically verified a fix that restores liveness.

The proof was checked against the implementation, not against a hand-written model of it: the artifact's sui_testcase.patch — applied over that very commit — adds a runnable simulation test at consensus/simtests/src/tests/my_simtests.rs that instantiates Sui's real Core component, delivers blocks in a carefully arranged order, and observes it jump straight to round 4 without creating a vertex in rounds 2 or 3 — the vulnerable behavior the trace above is built on.

The paper's abstract describes the manual layer: the authors "audited the current implementation of Mysticeti in the Sui blockchain and found it is susceptible to the described liveness bug." What it was not is a proof extracted from that source: the Rocq model is hand-written, not derived from Sui's Rust the way Aeneas and Charon derive Lean from Rust. Hence two halves, and an empty end-to-end cell.

No consensus system named in this post combines both halves of "end-to-end": a proof extracted straight from the real, unmodified production source, checked against an implementation actually running in the wild. Aeneas and Charon build the first half. Nobody has both, yet.

07 Five Recent Case Studies

Underneath the claims, the underlying trend is real: formal verification has been getting genuinely popular with blockchain implementers, and the breadth of the field is now hard to miss. Leonardo Alt's community-maintained Ethereum Formal Verification Overview tracks dozens of efforts, from ConsenSys's EVM-Dafny semantics and its Dafny formalization of the Eth2 beacon-chain spec to evm-sail's EVM semantics in the ISA language behind the official RISC-V model and powdr-labs' verified Yul-to-EVM compiler, the latter in Lean 4 — the same stack as this post's own quorum proof.

The five case studies below are worth taking seriously precisely because of that traction: the question was never whether the tooling has momentum, but whether the specific claims made about it survive scrutiny. Mysticeti is deliberately absent from that list: the original claim never cited it, so there is nothing here to fact-check — the one machine-checked proof in this post that engaged deployed code gets its own treatment earlier, in the unshipped-fix story and the end-to-end section.

Five named deployments get offered as evidence that formal verification has already moved from research exercise to production practice.

Read as a list, these five case studies do real work for the larger argument: they make formal verification sound like an established practice with a track record, not a speculative research direction.

One at a time:

1. Veil is described as a multi-modal verification framework layering model checking, SMT solving, and Lean 4 interactive proof into one pipeline. It's real, and its lead author, George Pîrlea, is correctly named — though the venue is CAV 2025 at the National University of Singapore rather than the "Lean FRO" attribution of the original claim, a minor misattribution rather than a fabrication.

2. Kaizen, attributed to Kalim et al., is the correctness-by-construction blockchain from FMCAD 2019: the consensus protocol at its core — plus a cryptocurrency, KznCoin, built on top of it — gets both its safety and liveness properties proved by a two-stage refinement, an abstract protocol verified in the Coq interactive theorem prover and refined through Dafny into imperative code, in the style of IronFleet, with the result benchmarked against stock Bitcoin. That makes it a genuine verification-from-inception case rather than a retrofit — though the citation matters: it's from FMCAD 2019, not 2021 as cited, which puts it six years before the "fifteen months of acceleration" window claimed above.

3. ChonkyBFT is ZKsync's committee-based BFT consensus engine for its sequencer network, built for single-slot finality and n ≥ 5f+1 fault tolerance; two theorems get described for it — quorum safety under arbitrary Byzantine action, and liveness after Global Stabilization Time.

   One mismatch worth flagging: the stack attributed to ChonkyBFT is "Lean 4 / Aeneas," but the real paper's own Section 5 formal-verification work — specifying the protocol and model-checking it — is done entirely in Quint, a TLA+-family specification language, checked with the Apalache model checker. The word "Lean" does not appear in the paper at all. ChonkyBFT is real, deployed on ZKsync Era mainnet, and formally specified — it just isn't a Lean 4 case study.

4. Multi-Chain / "Trinity Protocol" is cited for a specific, precise-sounding number — 184 machine-checked theorems, zero sorry placeholders, across Arbitrum, Solana, and TON. That figure is real, in the narrow sense that a post stating it does exist. What the citation elides is that its author, "Chronos Vault Team," is a single crypto-vault vendor writing about its own product, on a blog whose neighboring posts are titled "Trust Math, Not Humans" and "100% Formally Verified — Production Ready!" — vendor marketing copy, not an independently audited milestone, whatever the theorem count.

5. The Lean Ethereum initiative is described as a redesign of Ethereum's post-Merge Gasper protocol (Casper FFG plus LMD-GHOST) in Lean 4, covering SSZ serialization safety, post-quantum signature schemes (leanSig, leanMultisig), and fork-choice invariants tied to the 1/3-stake slashing margin. The OAK Research article cited for this is real. Ethereum's own formal-verification track record predates it by nearly a decade, and has nothing to do with Lean 4: Hildenbrandt et al.'s KEVM (CSF 2018) gave the EVM a complete K-Framework semantics, validated against the official test suite of more than 40,000 EVM programs, and Runtime Verification has used it commercially ever since to check real deployed contracts against properties like ERC-20 compliance. That lineage — KEVM, plus the EVM-Dafny and Eth2-Dafny work named above — is the actual multi-year history of Ethereum getting formally verified; none of it is what the "Lean Ethereum" citation is pointing to.

   The leanEthereum GitHub org itself is real, and worth a look on its own terms: it's the coordination hub for the roadmap's actual client implementations — zeam, ream, qlean, lantern, among others — plus supporting repos like leanSpec, leanVM, and leanMetrics. Multiple independent teams building multiple independent clients against one shared spec, before the protocol has even shipped, is the client-diversity pattern this post keeps returning to, playing out a second time in miniature — and it already has its own early shadow-network fuzzing harness, lean-shadow-fuzzer, running randomized simulation sweeps across those clients and charting block-propagation latency and finality.

   The Lean-4 connection gap is even starting to close for real: NyxFoundation's leanSpec-lean4, begun in April 2026, is an actual Lean 4 formalization of the leanSpec consensus specification, cataloging and proving propositions extracted from its SSZ, fork, validator, and networking layers.

Furthermore, nothing in this post's case studies involves Lean 4 code actually running in production:

• Aeneas and Charon extract in one direction only, Rust to Lean, so a refinement proof leaves the deployed binary exactly as Rust as it started — Lean 4 verifies it without ever touching the build.
• Lean 4's own compiler backend can produce a native binary directly, but no case study here uses it to do so.
• Kaizen makes the same point from a different angle, inside a single project: its own three-stage pipeline goes from Coq proof, refined to imperative Dafny, implemented in C# — three different languages, and the one that ships isn't the one that's verified.

08 Conclusions

Two separate questions were in play throughout: is the underlying technology real, and is the specific case built on top of it trustworthy. Those turned out to have different answers — and production consensus, running on Ethereum and Solana right now, turned out to be defended by neither Lean 4 proofs nor the citations presented here, but by client diversity and cross-client testing instead.

Strip out the parts that don't survive scrutiny and there's still a real, well-supported argument left standing: Lean 4 is a genuine engineering advance over Coq and Isabelle/HOL for this kind of work, Aeneas and Charon close a real and previously-unclosed gap between abstract protocol specs and the Rust binaries that actually run in production, and LeanDojo/ReProver-style retrieval-augmented tactic generation is a real, citable direction for lowering the labor cost of interactive proof. None of it needed the exaggeration it got.

That formally verified synthesis engine in Figure 17 — the arrow running straight from spec to proven code — is exactly the gap that stays open: nobody in this post generates a production consensus implementation directly from a Lean 4 spec, only proves one after the fact. Closing it is real engineering work still ahead, not a rounding error. What's genuinely new is that AI-orchestrated tactic generation and proof search give that work tools the pre-LLM era simply didn't have.

None of this means formal verification is oversold as a category — Jepsen-style chaos testing has a well-documented ceiling, and machine-checked proof genuinely raises the floor above it. It means the correct response to "trust the math, not the humans" is the same standard blockchain consensus itself gets held to here: check the math, and check who's telling you it checks out.

References

• Carrone, F. (2026). "A Proof Is Only as Good as Its Spec." Available at: federicocarrone.com
• Castro, M., & Liskov, B. (2002). "Practical Byzantine Fault Tolerance and Proactive Recovery." ACM Transactions on Computer Systems (TOCS), 20(4), 398–461. Available at: dl.acm.org
• Castro, M., & Liskov, B. (1999). "A Correctness Proof for a Practical Byzantine-Fault-Tolerant Replication Algorithm." Technical Memo MIT/LCS/TM-590, MIT Laboratory for Computer Science. Cited for the I/O-automata formal proof PBFT's Section 4.5 sketches and defers to. Available at: microsoft.com/research
• Chronos Vault Team. (2025). "184 Theorems, Zero Sorry: How We Formally Verified a Multi-Chain Protocol." Available at: dev.to
• de Moura, L., & Ullrich, S. (2021). "The Lean 4 Theorem Prover and Programming Language." Proceedings of CADE-28, LNCS 12699, 625–635. Available at: dl.acm.org
• França, B., Kolegov, D., Konnov, I., & Prusak, G. (2025). "ChonkyBFT: Consensus Protocol of ZKsync." Available at: arXiv:2503.15380
• Kalim, F., Palmskog, K., Mehar, J., Murali, A., Gupta, I., & Madhusudan, P. (2019). "Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity." FMCAD 2019. Available at: madhu.cs.illinois.edu
• Lamport, L. (1998). "The Part-Time Parliament." ACM Transactions on Computer Systems (TOCS), 16(2), 133–169. Available at: lamport.azurewebsites.net
• OAK Research. (2026). "Lean Ethereum: The Biggest Overhaul of Ethereum Since The Merge." Available at: oakresearch.io
• Pîrlea, G. (2025). "Veil: Multi-Modal Verification of Distributed Protocols." CAV 2025. Available at: lean-lang.org

• Hildenbrandt, E., Saxena, M., Zhu, X., Rodrigues, N., Daian, P., Guth, D., Moore, B., Zhang, Y., Park, D., Stefanescu, A., & Roșu, G. (2018). "KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine." IEEE 31st Computer Security Foundations Symposium (CSF), 204–217. Available at: fsl.cs.illinois.edu
• Munene, K. (2026). "Solana Urgent Patch Reveals How Easily Hackers Could Have Stalled Network." CoinCentral. Available at: coincentral.com
• Syme, D. (2026). "Lean Squad: Exploring Automated Software Verification with Near-Zero Human Labour." Available at: dsyme.net

• AbsInt. "The Structure of CompCert." Cited for CompCert's proof size and reported effort (100,000 lines of Coq, six person-years). Available at: absint.com
• Charon — Rust MIR-to-LLBC extraction frontend. Available at: github.com/AeneasVerif/charon
• Danezis, G. (2026). "Related Work: Consensus on Uncertified DAGs." lean-dag documentation. Available at: github.com/gdanezis/lean-dag
• Ho, S., Protzenko, J., & Fromherz, A. (2022). "Aeneas: Rust Verification by Functional Translation." Proceedings of the ACM on Programming Languages, ICFP 2022. Available at: dl.acm.org
• Jones, E., & Knottenbelt, W. (2026). "Towards Automating Blockchain Consensus Verification with IsabeLLM." Available at: arXiv:2601.07654
• Lamport, L. (2002). Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. Available at: lamport.azurewebsites.net
• lean-shadow-fuzzer (kamilsa) — Randomized Shadow-network simulation sweeps across Lean Ethereum consensus clients. Available at: github.com/kamilsa/lean-shadow-fuzzer
• leanEthereum — GitHub org for the Lean Ethereum protocol-simplification roadmap's client implementations and supporting specs (leanSpec, leanVM, leanSig, leanMetrics). Available at: github.com/leanEthereum
• NyxFoundation. leanSpec-lean4 — Lean 4 formal verification of the leanSpec Ethereum consensus specification. Available at: github.com/NyxFoundation/formal-leanSpec
• Yang, K., Swope, A., Gu, A., et al. (2023). "LeanDojo: Theorem Proving with Retrieval-Augmented Language Models." NeurIPS 2023 (Datasets and Benchmarks). Available at: arxiv.org
• Yin, M., Malkhi, D., Reiter, M. K., Golan Gueta, G., & Abraham, I. (2019). "HotStuff: BFT Consensus in the Lens of Blockchain." Cited for Algorithm 3's pseudocode. Available at: arXiv:1803.05069
• Z3 — Microsoft Research's SMT solver, used as a Lean 4 tactic backend. Available at: microsoft.com/research

• Alturki, M. A., Chen, J., Luchangco, V., Moore, B., Palmskog, K., Peña, L., & Roșu, G. (2019). "Towards a Verified Model of the Algorand Consensus Protocol in Coq." FM 2019 International Workshops, LNCS 12232, 362–367. Available at: arXiv:1907.05523
• Amoussou-Guenou, Y., del Pozzo, A., Potop-Butucaru, M., & Tucci-Piergiovanni, S. (2019). "Dissecting Tendermint." NETYS 2019. Available at: arXiv:1809.09858
• Carr, H., Jenkins, C., Moir, M., Miraldo, V. C., & Silva, L. (2022). "Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda." NASA Formal Methods 2022. Available at: arXiv:2203.14711
• Cosmos Hub v17.1 Chain Halt Post-Mortem (2024). Available at: forum.cosmos.network
• Dong, Z., Xu, X., Zeng, Y., Wan, M., & Li, C. (2025). "Universally Composable Termination Analysis of Tendermint." Available at: arXiv:2510.01097
• Galois, Inc. (2021). "Formally Verifying the Tendermint Blockchain Protocol." Ivy-based safety and accountable-safety proof, with an independent TLA+/Apalache formalization by Informal Systems. Available at: galois.com
• Interchain Foundation. (2019). "Cosmos Hub to Launch Mainnet." Available at: blog.cosmos.network
• Jehl, L. (2021). "Formal Verification of HotStuff." Proceedings of FORTE 2021 (DisCoTec 2021), 197–204. Available at: inria.hal.science · talk: YouTube
• Kukharenko, V., Ziborov, K., Sadykov, R. F., & Rezin, R. M. (2021). "Verification of HotStuff BFT Consensus Protocol With TLA+/TLC in an Industrial Setting." SHS Web of Conferences, 93, 01006. Available at: doi.org
• Xu et al. (2025). "Formal Modeling and Verification of Blockchain Consensus Protocols: A Case Study on ChainMaker." ICFEM 2025. Available at: link.springer.com

• BlockEden.xyz. (2026). "Solana's Client Diversity Moment: Firedancer, Agave, and the Race to One Million TPS." Available at: blockeden.xyz
• CoinDesk. (2024). "Bug on Ethereum's Nethermind Software Sparks Discussion of Client Diversity Risks." Available at: coindesk.com
• consensus-spec-tests — Common test vectors for the Ethereum proof-of-stake consensus layer. Available at: github.com/ethereum/consensus-spec-tests
• Ethereum Foundation. "Client Diversity." Available at: ethereum.org
• Hive — Ethereum end-to-end cross-client test harness. Available at: github.com/ethereum/hive
• Jordan, R. (2020). "Eth2 Medalla Testnet Incident." Prysmatic Labs. Available at: medium.com

• Feng, Z., & Zhang, R. (2026). "Survey of Consensus Protocol's Formal Verification." Cybersecurity. Available at: link.springer.com
• Gilbert, S., & Lynch, N. (2002). "Brewer's Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web Services." SIGACT News, 33(2). Available at: dl.acm.org
• Kingsbury, K. Jepsen: Distributed Systems Safety Analysis. Available at: jepsen.io
• Lamport, L., Shostak, R., & Pease, M. (1982). "The Byzantine Generals Problem." ACM Transactions on Programming Languages and Systems, 4(3), 382–401. Available at: lamport.azurewebsites.net
• Ongaro, D., & Ousterhout, J. (2014). "In Search of an Understandable Consensus Algorithm." USENIX ATC 2014. Available at: raft.github.io
• Wilcox, J. R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M. D., & Anderson, T. (2015). "Verdi: A Framework for Implementing and Formally Verifying Distributed Systems." PLDI 2015. Available at: homes.cs.washington.edu

• Andresen, G. (2013). "BIP 50: March 2013 Chain Fork Post-Mortem." Available at: github.com/bitcoin/bips
• National Vulnerability Database. (2010). "CVE-2010-5139." Available at: nvd.nist.gov
• National Vulnerability Database. (2020). "CVE-2020-26241." Available at: nvd.nist.gov
• "Value Overflow Incident." Bitcoin Wiki. Available at: en.bitcoin.it

• Moraru, I., Andersen, D. G., & Kaminsky, M. (2013). "There Is More Consensus in Egalitarian Parliaments." SOSP 2013. Available at: cs.cmu.edu
• Polyanskii, N., Mueller, S., & Vorobyev, I. (2025). "Starfish: A High Throughput BFT Protocol on Uncertified DAG with Linear Amortized Communication Complexity." Cryptology ePrint Archive, Paper 2025/567. Available at: eprint.iacr.org
• Qiu, L., Xiao, J., & Shao, Z. (2026). "Mechanized Safety and Liveness Proofs for the Mysticeti Consensus Protocol under the LiDO-DAG Framework." IEEE Symposium on Security and Privacy (S&P) 2026. Available at: zenodo.org
• Ryabinin, F., et al. (2025). "Making Democracy Work: Fixing and Simplifying Egalitarian Paxos." OPODIS 2025. Available at: drops.dagstuhl.de
• Sutra, P. (2020). "On the Correctness of Egalitarian Paxos." Information Processing Letters, 156, Article 105901. Available at: arXiv:1906.10917