Formal Verification

What you’ll get here

what we actually proved about the protocols that keep a permissionless validator set safe, what that proof does and does not cover, the defects the proofs found in our own production code — and the command that lets you re-run the results yourself.

Most platforms tell you they were audited. An audit is a smart human reading code for a few weeks. It is valuable, and it is a sample — a reviewer cannot read every interleaving of a distributed system, because there are billions of them.

Formal verification attacks the other half of the problem. Instead of sampling, you write a mathematical model of the protocol and let a model checker exhaustively check every possible execution within a bound — every ordering, every crash point, every partition, every message reordering — or, where that is intractable, run tens of thousands of random executions of the model. If a safety property can be broken, the checker returns the exact sequence of steps that breaks it.

We did this for the protocols that matter most for open participation: validators joining and leaving a live network without breaking key custody, consensus, or data durability.

---

Why this matters for permissionless

While the validator set is fixed, most of these protocols are never stressed. The moment anyone can join or leave, every one of them runs concurrently with membership churn — and that is where distributed systems historically fail. The famous cases are not exotic cryptography breaks; they are reconfiguration bugs. Raft’s original membership-change algorithm was shown unsafe this way. ZooKeeper’s reconfiguration carried a bug for years that testing never caught and a model checker did.

We would rather find ours with a solver than on mainnet.

---

What we verified

Seven protocols, modelled in nine Quint specifications. Some properties are checked with Apalache, a symbolic model checker that proves a property holds for all executions up to a bounded depth (not a sample of them). Others, where Apalache is not tractable, are checked by Quint’s simulator over tens of thousands of random executions; that is strong evidence, not a bounded proof. specs/README.md in the verification bundle states which method backs each property.

Protocol	Safety properties proven to hold
Proactive resharing	The group secret is preserved across a reshare; shares from two different epochs can never be combined; the participant list is only rotated once every new holder durably has a share; a node never deletes a share it still needs.
Validator membership	No membership change is applied without a quorum of distinct, currently-active, cryptographically verified approvals; no unauthenticated node can enter the signing set.
Genesis cold-boot	Exactly one leader; the bootstrap body runs at most once network-wide; a node joining later can never re-trigger it.
Signing gate	Deny-totality — every error, timeout, cache miss, missing dependency or unrecognised operation results in a refusal to sign. Checked exhaustively with Apalache over the modelled decision tree.
Threshold signing (FROST)	A signing nonce is never used twice; a validator only ever signs over its own unmodified commitment; only the frozen quorum’s shares aggregate.
Durability under churn	At most one write-master per app per term; every referenced content hash stays pinned by at least k live nodes across any sequence of joins and leaves.
Secrets under churn	No encrypted record is ever orphaned by a key rotation; no attestation signer is ever counted twice toward a quorum.

---

What formal verification actually produced

This is the concrete output — four artifacts, not a slogan.

1. Executable specifications. The protocols now exist as precise, machine-readable models, not prose in an architecture doc. Ambiguity that survives in English does not survive in a model — writing them forced several under-specified behaviours into the open.

2. Machine-checked results. The properties in the table above are checked by a machine — bounded proofs with Apalache where tractable, large random simulations otherwise — and are re-runnable on demand. Nobody has to take an engineer’s word that “resharing preserves the group key.”

3. Counterexample traces — the defects it found. When a property does not hold, the checker prints the exact step-by-step execution that breaks it. This is where the real value showed up: model checking surfaced 13 classes of defect in our own production code, each as a reproducible trace, including —

• a key-rotation sequence that left encrypted data permanently unreadable;
• a network partition where two halves each elected a write-master for the same app (split-brain);
• an amendment path where an old, superseded ruleset could be replayed, and a vetoed rule kept being honoured;
• two concurrent membership changes that silently clobbered each other’s participant set;
• a distributed key generation ceremony where a malicious participant could send different values to different validators, leaving honest nodes with different group keys;
• content addressed by on-chain state that could end up pinned nowhere.

Here are all thirteen, so the count is auditable rather than asserted. The *Fixed modules named below are in the verification bundle’s specs/ folder and re-verify whenever the verification script is run.

#	Defect	Where it was closed	Status
1	Genesis elects two leaders from divergent local views	genesisBootFixed	fixed
2	Genesis bootstrap body reachable twice inside one catch-up window	genesisBootFixed	fixed
3	Genesis ceremony parametrised by a leader’s strict-subset view	genesisBootFixed	fixed
4	Attestation slot-rollback liveness gap	attestationFixed	fixed
5	KEK generation retired with envelopes still sealed under it	kekChurnFixed	fixed — see the note below
6	Superseded ruleset replayable; vetoed rule still honoured	amendmentWalkFixed	fixed
7	Reshare-binding lost update (two executors, last writer wins)	membershipGovernanceCasFixed	fixed
8	Membership reorder divergence on re-join after removal	membershipGovernanceConvergent	fixed
9	Membership quorum view-skew across replicas	membershipGovernanceAnchored, checkpointLogUnique	fixed — flag off by default
10	BaaS split-brain write-master under partition	durabilityFixed	fixed
11	No enforced IPFS replication floor — content pinned nowhere	durabilityFixed	fixed
12	Replicas compute different state roots from the same writes	property tests (no model)	fixed
13	Restarted oplog producer reuses sequence numbers	property tests (no model)	fixed

Two things this table is deliberately not hiding. Row 5 ships a re-wrap action and a retire guard that the retire path must call; today nothing calls either, because the generation lifecycle they protect is itself dormant — production is pinned at generation 1, so there is no previous generation to orphan. The mechanism is built and tested ahead of the rotation that will need it, and wiring one without the other would reopen the defect. Row 9 is the flag case described below. And two findings are not in the table. One is a failure-detector divergence where a partitioned node evicts a peer its cohort still considers live: it has no fix module, it still reproduces, and we count it as open rather than quietly folding it into thirteen. The other is last-mover key bias in the DKG ceremony (a participant who sends last can bias the resulting key): it was closed as a scope decision, not fixed, and the model keeps it as a known, reproducing violation.

All thirteen are fixed. Eleven were re-checked against the same model that produced the counterexample, until the property reports clean. Two — the replica state-root divergence and the oplog sequence reuse — surfaced in the property-based test tier rather than the model checker, and were closed there: the tests that pinned them as known failures are now ordinary passing tests. There is no Quint model of either, so for those two the evidence is exhaustive-over-generated-inputs, not bounded-exhaustive over executions. The last one took eight independent adversarial reviews to close, and it is worth saying why: the obvious fix — pinning the trusted validator set into the change itself — is circular, because the approvals that would authenticate that set are exactly the approvals it gates. The next idea, anchoring on an existing on-chain registry whose write key is threshold-held, fails for a subtler reason that is the single most useful thing we learned: a threshold signature proves the quorum signed the transaction, not that it agreed with the contents. The working answer is an append-only membership checkpoint whose entries honest peers refuse to co-sign unless the body matches a quorum-approved change, with each entry bound to its position in the chain so a replayed entry is inert by construction.

⚠️ One caveat we state rather than bury

The fix for row 9, membership quorum view-skew, ships behind a switch that is off by default. Turning it on needs a checkpoint topic with a threshold-held write key, and the genesis validator set that the chain’s first entry is verified against; the first membership change then writes the chain root automatically. Until both are done the anchored path is inert and quorum eligibility still reads each node’s local view — so the defect is fixed and verified, not yet in effect. We would rather say that than let a merged-but-dormant switch be counted as a live guarantee.

The verification pass also caught a defect in its own integration: an independent review of the branch merge found that one newly-added message subject consulted an unbound registry, silently disabling its origin check. That would have let an attacker suppress a peer’s message and defeat one of the very defences this work added. Found, fixed, and covered by a regression test before merge — which is the point of reviewing your own work adversarially.

4. A re-runnable regression check. The models are not a one-off report — they ship with a verification script that pairs each fixed model with its pre-fix counterpart, so a fix that stops being load-bearing makes the script fail. The script is run by hand today; no CI job runs it.

🧠 For Normies

Think of a flight simulator for the network’s rulebook. Instead of flying the plane a thousand times and hoping you hit the bad case, the simulator tries every combination of things going wrong — a validator vanishing mid-handshake, two operators acting at the same instant, the network splitting in half — and reports the exact sequence that would break it. We ran it, it found thirteen real problems, and we fixed all thirteen — though the last fix is switched off until an operator turns it on, which is the honest version of “fixed”.

---

What this does not claim

We state the boundaries plainly, because a formal-methods claim without its scope is marketing.

Caution

• This is not “the platform is proven correct.” We verify models of the protocols, plus property tests that run against the real code. There is no tool that proves an entire TypeScript codebase correct, and anyone claiming otherwise is selling something.
• The proofs are bounded, and some results are simulation only. The Apalache proofs are exhaustive up to a set number of nodes, faults and protocol steps (typically 3–5 validators, one faulty node, and up to a dozen steps). Properties where Apalache is intractable are backed by random simulation, which samples executions rather than covering all of them. Protocol-logic defects almost always appear at small scale — that is the established result the method relies on — but a bounded proof is not an unbounded one.
• Everything is conditional on the fault assumption. The proofs hold given that no more than the tolerated fraction of validators is malicious. Keeping that true in an open network is a matter of economics — staking, membership gating, reputation — not something a solver can establish.
• Property-based tests sample; they do not prove. They run the real cryptographic code across thousands of generated inputs. That is strong evidence, not a proof.

Everything above is a real limit of the method, honestly stated. Within those limits, the results are machine-checked and reproducible — which is more than a code audit alone can offer.

---

Verify it yourself

The point of this work is that you do not have to trust our summary of it. The models describe protocol behaviour only and contain no implementation code, so they can be published on their own as a verification bundle that anyone can re-run.

Not public yet

The bundle is not published yet. The pre-fix model of row 9 is a working recipe against the default configuration, so it stays private until that fix is switched on in production.

Once the bundle is out, re-running it takes two commands:

npm i -g @informalsystems/quint
bash specs/verify.sh

The script type-checks every model, re-runs each property with Quint’s simulator on a pinned seed — checking that it still holds on the fixed model and still breaks on the pre-fix one — and runs the recorded-trace conformance tests. It does not run Apalache. The bundle’s README lists the exhaustive Apalache proofs with their exact commands and search depths; those need Java 17 or later, and Quint fetches Apalache automatically.

---

How it fits the rest of this section

Formal verification is the evidence layer underneath the guarantees described elsewhere in this section: TSS / MPC explains how key custody is split, and the resharing and threshold-signing proofs above are what demonstrate that the split survives validators coming and going. Threat Model states what we defend against; the counterexample traces are where we found places we did not, yet.

Related: Threat Model · TSS / MPC · DKG & Threshold Signatures · Zero Single-Signature