The Case for Verified Consensus, Part 1

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 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 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 the form the kernel can check. They are 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. 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. 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. 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 a quick pause 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 a project of its own then, and often still is, 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. The Lean 4 end of it is already the bleeding edge in practice, not just in theory; the Mysticeti formalization in Part 2 will make that 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 bugs, the ones 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 or AI-orchestrated tactic generation, is how Ethereum or Solana actually defend against the bugs 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. That's 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. A passing test there means the code handles real mainnet parameters. The minimal configuration scales every parameter down, a handful of validators and 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 isn't hypothetical: a deviating client exposed and contained by disagreeing with the majority. 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

Grading the remedy means grading it against something. Every consensus protocol specification rests on two properties Leslie Lamport formalized in the 1970s: safety, meaning nothing bad happens, and liveness, meaning something good eventually happens.

Safety for a consensus protocol unpacks into agreement, validity, and integrity. Agreement means no two honest nodes decide differently for the same slot; validity means a decided value must trace back to a legitimate proposal; integrity means no node decides twice. Liveness unpacks into termination and progress: every honest node eventually decides, and 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. It isn't a free pick-any-two. During a partition it's a hard choice between consistency, all nodes seeing the same data and therefore a safety property, and availability, every request getting a response and therefore a liveness property.

Public blockchains sit at the extreme consistency-over-availability end, stopping finalization when the network splits rather than risking two histories. That's 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 and a handful of rounds. Past that, they run into the state space explosion problem almost immediately.

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. That's a different problem from 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, like "node i has locked block B at round r," have to compose into global facts across the whole quorum structure. The standard BFT quorum-intersection lemma is the canonical example: any two quorums of size ⌈(2n+1)/3⌉ share at least one honest node. The quorum-intersection proof in Part 2 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. That history 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. Those are 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, but they are not the same claim as a machine-checked proof that holds for arbitrary n. 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. Their test case against the actual deployed implementation found it incorrect, in a way that can lead to real liveness attacks.

Here's the specific bug: 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. The naïve framing, battle-tested and 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. They used 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 on 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. It 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 checks whether the spec itself says what the protocol designer meant it to say. Not the prover's kernel, not the extractor, not a zero-sorry refinement proof.

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." That's 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. Carrone put the same point 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 rather than 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; the spec drew its boundary in the wrong place, and the proof of the model it did cover was never broken. HotStuff's formalizations prove the abstract algorithm, not the Rust or Go a validator actually runs, a boundary between model and code rather than between correct and incorrect reasoning. 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. Stubbornly under-specified systems pass every check you thought to run, right up until the one you didn't.

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
• 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
• 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

• 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
• Lamport, L. (2002). Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. Available at: lamport.azurewebsites.net
• 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

• 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

• 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