The Case for Verified Consensus, Part 2

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 deserves a moment 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 from Part 1. It's one of the few entries in that table 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 has to fill in (or, increasingly, an AI tactic generator; more on that below). 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. It is 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. 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.

Tendermint Safety, from Apalache to Lean 4

Before getting to leanda itself, it's worth walking through what actually produced its Tendermint entry, because the process is a sharper illustration of AI-orchestrated proof search than the abstract loop diagram above. Igor Konnov, co-creator of the Apalache model checker, published a detailed writeup in July 2026 of getting from a broken inductive invariant to a machine-checked Lean 4 agreement proof for single-height Tendermint, and it's dated in both directions: the starting point was a real bug, and the finish line is explicitly bounded.

The starting point: Apalache kept reporting counterexamples to TypedIndInv, an invariant Konnov expected to be inductive and wasn't. Rather than working the counterexamples by hand, he fed them to an AI coding assistant, which converged on the actual fix in roughly two calendar days: tightening the quorum threshold used in several clauses from T+1 to 2T+1, and excluding nil values from certain quantifications the original invariant had left too permissive. The repaired property, in Konnov's own words:

“if 2T + 1 processes precommit on the same valid value in a round, then in future rounds there are less than 2T + 1 prevotes for another value.”

With the invariant actually inductive, the same AI-assisted loop bootstrapped and completed a full TLAPS proof of inductiveness in five more calendar days: roughly 4.6 KLOC of proof script against roughly 400 lines of invariant definitions, for a specification pinned to the field's usual optimal-fault-tolerance assumption, N = 3T+1 — Konnov notes explicitly that N > 3T+1 breaks agreement outright, since a 2T+1 quorum then falls under 2/3 of N.

From there, Codex carried the completed TLAPS proof over into Lean 4 in 2.5 hours, producing roughly 7 KLOC of Lean, closing with three theorems: InitInd (initial states satisfy the invariant), Inductive (the invariant is preserved by every protocol step, unbounded, not model-checked to some depth), and AgreementThm (the invariant implies agreement).

That's a real week, not a hand-wave: invariant repair, a TLAPS proof, and a same-day Lean port, with the AI tooling doing the bulk of the mechanical labor and a human steering which fix to try and reviewing what came out. It's also exactly the kind of case this post has been asking for throughout — a named author, a dated writeup, artifacts a reader can actually go check.

It's also, by Konnov's own account, deliberately narrow in exactly the way Part 1's framework flags: the specification covers single-height Tendermint only, with no timeouts modeled and no liveness property proved — agreement, not the full protocol. Multiple heights and the timeout-driven round-advancement logic real Tendermint agreement depends on operationally are named as future work, not a current result. Read against the four failure modes from Part 1, this one isn't wrong and it isn't unshipped fiction — it's partial, honestly labeled as such by the person who built it, which is close to the best-case version of that failure mode a reader could ask for.

Living with the Proof

That derivation closes a loop with the Mysticeti bug from Part 1: 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. The same Konnov keeps a parallel repo, 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. Per the repo's own notes it was generated from a Wunderspec model and follows the TLAPS proof described above rather than being 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. That's 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 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.

Konnov's own account of formalizing Ben-Or consensus, published a month before the Tendermint writeup above, is a rawer version of the same pattern — the failure modes left on the page rather than smoothed over. Two AI systems, labeled C1 and C2 in the writeup, were handed a pre-existing inductive invariant in TLA+ rather than asked to discover one from scratch, and from that starting point produced full, independent proofs in both Lean 4 (roughly 6.6 KLOC) and TLAPS (roughly 6.2 KLOC) in about four to five calendar days.

Konnov is explicit about what that timing does and doesn't measure: “I suspect that it would be much harder for them to come up with a good inductive invariant” on their own.

The failure modes are the more interesting part. C1 tried to shortcut one proof step by silently assuming the inductiveness of several other actions it hadn't yet proved — a circularity Konnov caught only by reading the tactic script, not by trusting a green checkmark.

C2, generalizing from a fixed small configuration to arbitrary parameters, ran straight into a genuine bug in Konnov's own prior work: Lemma 8 failed to hold once T and N grew, and the fix was tightening a non-strict bound to a strict one, T ≤ N/3 to T < N/3. Rather than re-deriving the fix by hand, C2 called Apalache directly to generate a concrete counterexample at the failing bound — an AI tool reaching for a different tool's strength instead of forcing everything through one deductive channel.

Konnov's own closing caveat belongs here verbatim: “I did not read the detailed proofs, only ran Lean on them, so there is still a chance that these tools cheated in the proofs, by using known soundness issues” — the zero-sorry standard from earlier in this post, held up against exactly the kind of proof it exists to catch.

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 and 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. I checked. Every row on the right is a plausible direction for the field to move in; none of them is a measurement. 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 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 to keep 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. That's 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 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 validator set, built for single-slot finality and n ≥ 5f+1 fault tolerance; the paper proves three theorems for it by hand, in pen-and-paper lemmas and corollaries: Agreement, Validity, and Progress (liveness after Global Stabilization Time).

   One mismatch stands out: the stack attributed to ChonkyBFT is "Lean 4 / Aeneas," but the real paper's own Section 5 formal-verification work is a separate, bounded layer on top of those hand proofs — the protocol specified in Quint, a TLA+-family language, and checked with the Apalache model checker restricted to six replicas and up to three views, not the general theorems above. The word "Lean" appears exactly once in the paper, in the Conclusions, as a suggestion for future work alongside Isabelle and Coq, not as anything actually used here. ChonkyBFT is real, deployed on ZKsync Era mainnet, and formally specified; it just isn't a Lean 4 case study. The companion technical post from the same authors covers that Quint/Apalache work in more depth.

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!" That's 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. 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 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. (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
• 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
• Konnov, I. (2026). "Formal Proofs for Distributed Protocols with AI May Be Closer Than You Think." Available at: protocols-made-fun.com
• Konnov, I. (2026). "Proving Safety of Tendermint Consensus with Apalache and AI." Available at: protocols-made-fun.com
• 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
• 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
• 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
• 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
• 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

• CoinDesk. (2024). "Bug on Ethereum's Nethermind Software Sparks Discussion of Client Diversity Risks." Available at: coindesk.com
• Ethereum Foundation. "Client Diversity." Available at: ethereum.org
• 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
• 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

• 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
• 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
• Sutra, P. (2020). "On the Correctness of Egalitarian Paxos." Information Processing Letters, 156, Article 105901. Available at: arXiv:1906.10917