How do you know?
In 1970, Edsger Dijkstra wrote down the most uncomfortable sentence in software engineering: testing shows the presence of bugs — never their absence. The crash lab rehearses this system's disasters thousands of times, and Dijkstra's objection still stands. For the handful of properties that must not fail even once, there is a stronger tool: rewrite the protocol as mathematics and check every case at once. That work is underway. What follows is the tool itself, why it matters, and — honestly — how far it has gotten.
Five missing cells
In the summer of 1994, Thomas Nicely, a mathematics professor in Virginia, was computing the reciprocals of twin primes on a brand-new Pentium. His sums came out subtly wrong. He spent months eliminating suspects — his code, his compilers, his other machines — until only one remained: the processor itself. Deep in the chip's division circuitry sat a lookup table missing five entries out of roughly a thousand. The flaw corrupted about one division in nine billion.
Here is the uncomfortable part: Intel had tested that chip with extraordinary thoroughness — and had even found the bug in-house, judged it too rare to matter, and shipped. At one error per nine billion random divisions, that judgment was statistically defensible. The public declined to take the actuarial view. The recall cost $475 million, and the industry drew the enduring conclusion: within a few processor generations, arithmetic units weren't tested into confidence anymore — they were proven, every table entry, every input, every case.
"Program testing can be used to show the presence of bugs, but never to show their absence." — Edsger Dijkstra, 1970.
Twenty-four years later, the invoice arrived.Every case at once
A test runs the system once and looks at what happened. A proof is a different kind of object entirely: an argument that covers every possible case simultaneously — not because someone ran them all, but because the argument's structure leaves no case out. The practical workhorse between the two is the model checker: you write the protocol's rules in a precise mathematical notation — a model — state a property ("no two honest replicas ever commit different blocks"), and a tool explores the entire space of behaviors the rules permit: every message ordering, every timeout, every choice an adversary could make. Not a sample of the space. The space.
A test
Each run walks a single path through the possible and checks what it finds there. Fast, concrete, endlessly useful — and mute about the paths not taken.
The crash lab
Seeded adversarial simulation walks thousands of paths, deliberately hostile ones, each replayable forever. The best presence-of-bugs machine we know how to build — and still, a sample.
A checked model
The model checker holds the whole space at once. It returns one of exactly two things: the property holds everywhere it looked — or a counterexample.
The counterexample deserves emphasis, because it's what makes this engineering rather than philosophy. A failed check isn't a red X and a shrug — it is a concrete attack script: deliver this message before that one, time out here, have this validator do exactly this, and the property falls. You can hand it to an engineer. Better: you can hand it to a simulator.
Five load-bearing walls
Why does a blockchain, of all things, warrant this effort? Because consensus protocols are precisely where testing is weakest and stakes are highest. The bugs live in freak interleavings — a timeout landing between two messages that "always" arrive together, a partition healing at the one wrong moment of an epoch — and the field's history is humbling: protocols published, peer-reviewed, and deployed have had safety flaws surface years later, several found only when someone finally wrote the model. And unlike an application bug, a consensus bug isn't a malfunction; it's a fork — the one thing that must never happen.
So the system keeps a register: every safety and liveness property it claims, written down with a stable name — built deliberately as a verification worklist, not documentation garnish. At its core sit five properties — the walls everything else leans on:
No forks. No two honest replicas ever commit different blocks at a height — the overlap.
No half-payments. A cross-shard transaction ends the same way on every shard it touches — the generals.
No one-sided settlements. …even when one of those shards ceases to exist mid-flight — the will.
No ambiguous authority. Every honest machine derives the identical committee for any moment it can encounter — the clock and the census.
No lost state. Splitting and merging shards never loses, invents, or re-homes a single record — the library.
Everything else in the architecture — the sync machinery, the caches, the archive, the triage — exists to keep those five true under real networks and real adversaries. They are the properties worth the strongest tool we can bring.
From register to rehearsal and back
Most systems attempting this face an archaeology problem: the "protocol" exists only as code tangled with sockets, threads, and clocks, and building a faithful model means excavating it. Hyperscale skipped that fate by construction — the crash lab's precondition is the same as the model's: every protocol component is already a pure transition function with explicit inputs. Extracting a model is translation, not archaeology. The specs are written in Quint — a modern notation from the TLA+ family, the lingua franca of protocol verification — and checked with Apalache, a model checker that explores the state space symbolically rather than one state at a time.
And the loop has already earned its keep. While the beacon's agreement protocol was being modeled against the algorithm it implements, the checker surfaced a real divergence: in one corner case, the implementation walked its history subtly differently from the paper — legal-looking, wrong under exactly the right absence of data. The model produced the recipe; the deterministic simulator replayed the recipe as a failing test; the fix landed with a permanent regression pinning it. No user ever saw it. That round trip — model finds, simulator reproduces, fix verifies — is the whole method in one anecdote.
What is and isn't being claimed
A worklist, not a trophy case
First-pass models of the critical core exist and are being checked today. That is not a claim of "proven" — the register is a to-do list, being worked through in the open.
Fidelity is its own discipline
The checker certifies the mathematics; keeping the mathematics and the Rust in agreement is a separate obligation — made tractable because the code is already pure transition functions, and kept honest by replaying every model counterexample against the real implementation.
Small worlds, searched completely
Model checking explores everything inside explicit bounds — small committees, short horizons. The bet, backed by decades of practice: protocol bugs have small witnesses. Unbounded proofs of the deepest properties are the long game, not the current claim.
The ladder of certainty: tests walk one path; the crash lab walks thousands of hostile ones; a checked model holds all of them at once, inside its bounds; a proof removes the bounds. Each rung catches what the rung below can only sample.
Dijkstra's sentence still stands — testing will never show the absence of bugs. The point of this program is to make that stop mattering: one named property at a time.