A Lean 4 + Mathlib formalization of the finality mechanism of Casper FFG, the component of the Gasper protocol (Buterin et al., 2020) that guarantees irreversibility of finalized blocks in the Ethereum Beacon Chain.
Three core properties of Casper FFG are formally verified:
If two conflicting blocks are both finalized — meaning the protocol has committed to two incompatible histories — then every validator in the intersection of the two supporting ⅔-quorums has provably violated a slashing condition:
- (S1) Equivocation — two votes to distinct targets at the same height.
- (S2) Surround vote — one vote's source–target span strictly contains another's.
The result generalises Casper FFG Theorem 1 (and Gasper Theorem 5.2) in two directions: from 1-finalization to arbitrary k-finalization, and from static to dynamic validator sets.
Regardless of past events, it is always possible to extend the protocol state and finalize a new block without introducing new slashing — provided the underlying blockchain keeps producing blocks and at least ⅔ of the stake is honest.
The quorum intersection that Accountable Safety forces to be slashed has quantitatively positive weight, with an explicit lower bound accounting for validator churn (activations and exits relative to a reference set):
This development translates and substantially extends the Coq formalization by Runtime Verification, Inc.
Key departures from the Coq version:
| Aspect | Coq version | This Lean 4 version |
|---|---|---|
| Axiom of choice | Used globally | Eliminated — proofs are constructive |
| Boolean relations | Defined as bool-valued functions |
Prop-valued inductive closures |
| Global axioms | Environment-level | First-class term-level values |
| Block existence predicate | Contains a bug | Corrected |
| Lemmas layer | Minimal | New: disjoint-union algebra, weight inclusion–exclusion, strong induction on height gaps |
Eliminating Classical.choice means all proofs elaborate to closed terms in the kernel's type
theory, making the theorems constructively valid and the predicates computationally executable
via decide.
The only non-constructive axioms present are Quot.sound and propext, inherited through
Mathlib's Finset infrastructure.
GasperBeaconChain/
├── Audit/ — axiom auditing and build verification tooling;
│ ├── Automated/ automated build audit (axiom-set checks run on every build)
│ └── Meta/ meta-commands: axiom reporting, JSON export, scope checks
├── Core/
│ ├── AtomicDef/ — validators, block trees, votes, slashing conditions,
│ │ quorums, justification, k-finalization, liveness hypotheses
│ ├── Lemmas/ — ancestry closure, set algebra, weight monotonicity,
│ │ quorum up-closure, strong induction, slashing constructions
│ └── Theories/ — AccountableSafety, PlausibleLiveness, SlashableBound
├── Executable/ — Boolean decision-procedure wrappers for all key predicates;
│ └── UseCases/ concrete runnable examples (fork scenarios, slashing detection)
└── Visualizations/ — interactive diagrams (justification ladders, Venn overlaps, …)
Each theorem in Theories/ is accompanied by a #detail_explode invocation that renders its
full Fitch-style proof tree in the live documentation.
Requirements: Lean 4 (leanprover/lean4:v4.31.0) and the Lake build tool (included with Lean).
# Fetch dependencies (Mathlib cache included)
lake update
lake exe cache get
# Build all proofs
lake buildLiterate HTML documentation (requires Verso):
make verso-pages # generates docs/ ready for GitHub Pages
# or, to preview locally:
make verso-facet # builds and serves at http://localhost:8000- V. Buterin et al., Combining GHOST and Casper, 2020.
- Runtime Verification, Inc., Beacon Chain Verification (Coq).
MIT — Copyright © 2026 Nyx Foundation and gasper-lean4 contributors.