lean-dag

Provenance. Code and prose in this project were co-written with heavy LLM assistance. The Lean proofs are machine-checked — the kernel verifies every theorem against its stated form — but whether the definitions and theorem statements capture their intended meaning, and whether the surrounding prose is faithful to what is proved, has only human-plus-LLM review behind it. Read critically.

A Lean 4 + Mathlib formalization of uncertified DAG consensus in the style of Mysticeti: the DAG itself, the commit rule, and machine-checked safety and liveness — together with further developments built on the same foundation, each in its own module consuming the core read-only. The core is stated for n ≥ 3f+1 validators with quorums of size n − f, over pipelined, multi-leader slot schedules; the variant arcs move the committee — n ≥ 5f+1 for two-round commitment, n = 3f + 2p − 1 for a fast path that tolerates p missing votes, n ≥ 5·fb + 3·fc + 1 for hybrid faults, and a bare majority at n ≥ 2f+1 for crash faults alone.

What is proved

• Safety of the Mysticeti-style commit rule — agreement across views and routes, uniqueness of the committed sequence, a monotone and agreed ledger — with no network assumption of any kind.

• Chain quality (LeanDag/Quality/): every commit's flush carries, at every round below it, blocks from at least half of the correct validators — with no synchrony assumption — and once the DAG is synchronous, every correct block enters the agreed ledger within a schedule-window of its creation; a six-validator counterexample shows the aggregate guarantee provably does not imply the individual one.

• Liveness above eventual DAG synchrony, a structural condition on the DAG under which no liveness theorem mentions time. The whole of what the network must supply reduces to a single clause of view convergence — after stabilisation, whatever one correct validator holds reaches every correct validator within Δ — from which the structural condition is derived, and block production with it, rather than assumed. The threshold a deployment must meet is the constant 2Δ + proc: no quantity set by deployment appears, because the pacemaker's catch-up rule collapses any clock spread to Δ + proc in one post-stabilisation round. And liveness is local — not merely that some view commits, but that every reliable validator decides on its own view, at an explicit time (commits_recur_local).

• Denial-of-service resistance (LeanDag/DoS/): safety is shown independent of any anti-equivocation condition; storage is bounded under an exposure condition (with a matching construction showing its exponential constant is forced) and made linear-forever under an enforceable, author-blind novelty budget (dos_resistance).

• Garbage collection (LeanDag/GC/): a per-validator horizon below which nothing is retained, with commit verdicts invariant across the cut, storage constant at a lag, bootstrap by an f+1-sampled attested base — and no consensus on the cut anywhere.

• Odontoceti (LeanDag/Odontoceti/): safety and liveness of the two-round commit rule (arXiv:2510.01216), generalized from n = 5f+1 to n ≥ 5f+1, on the unmodified DAG layer — including four findings about the published safety argument, one of which (agreement among indirect commits resting on candidate-iteration order) is refutable on data without the canonicity repair the formalization supplies.

• Reactive schedules (LeanDag/Reactive/): both commit rules remain live when validators wait only until they hold the leader's block — or, under Mysticeti, until they can certify — with the timeout as a fallback. The fast path is quantified: round latency is bounded by drift, delivery and processing with the timeout appearing nowhere, and when delivery undercuts the timeout no timeout ever fires.

• Catch-up, now a clause of the pacing core: drift between validators is preserved, not contracted, by the waiting rule alone — refuted on data — and the pacemaker's second rule (seeing evidence of a round is entering it) collapses any spread to Δ + proc in a single post-stabilisation round, whatever it was before; a witness starts with a spread of ten and collapses to exactly three. A valid block cannot outrun the honest schedule, so the author-blind rule a deployment runs is safe (exists_honest_floor).

• The view a validator holds (LeanDag/Mysticeti/PaceDelivery.lean): the commit rules are view-relative and the pacing line reasons about time-indexed holdings; the two are now joined. A validator's holdings are a view (viewAt_ids), which is what makes liveness local; and a pacing structure induces a delivery layer, so the storage model of the DoS arc is derived rather than postulated — including its acceptance rule, at most one block per author, which follows from the reference discipline (heldOf_inj). One structure plus the acceptance budget then yields liveness and linear storage together (dos_resistance_of_pace).

• Safe Skip (LeanDag/SafeSkip/): a crashed validator rejoins with one constant-size message denoting a block for every missed round — a donor's references plus the self reference the validity rules force. The fill is proved a block universe extending the old one unchanged; production is restored at every missed round, a filled leader candidate is directly skipped rather than committed, and every verdict reached before the fill re-derives and agrees after it (decided_fill_agree).

• Adaptive leaders (LeanDag/Adaptive/): a HammerHead-style schedule — the leaders ahead recomputed from the agreed prefix, to favour validators observed live — proved safe and live for any anchored rule. A configuration decides as far as the anchor that closes its span and outputs only to the span's own boundary, and that separation is what makes safety unconditional: two runs from one genesis configuration agree under no synchrony, fairness or window hypothesis, for arbitrary scores including adversarial ones (Barnacle.Agreement.holds). Liveness is the horizon of the timed arc with one more configuration supplied (Barnacle.Progress.holds), and what a reputation score owes the mechanism is four clauses and no more (Adaptive.Score.holds). The arc composes with the other mechanisms at any rule that reads its universes as block records, not per protocol: cuts compose beneath a configuration and stack with a recovery, and a fill or a re-genesis carries a whole run across and leaves its ledger the same list.

• Hybrid fault tolerance (LeanDag/Hybrid/): the two-round rule proved safe and live under separate Byzantine and crash caps — fb equivocators, fc honest validators that may halt — at Orcaella's bound n ≥ 5·fb + 3·fc + 1 (arXiv:2607.04789), for every indirect threshold in an admissible interval whose nonemptiness is the committee bound. Four validators suffice for two-round finality under a single crash, where Byzantine tolerance costs six; at fc = 0 the development collapses onto Odontoceti. The bound is also proved necessary: one validator short, one view derives conflicting verdicts at every threshold (hybrid_bound_necessary).

• Resilient checkpoints (LeanDag/Checkpoint/): explicit epoch-, height-, and history-bearing proposal messages are emitted from append-only per-validator protocol state. The layer is a mechanism in the sense of Properties/: it names no protocol. SigningFaults is what its counting needs of a fault model, a quorum threshold, the reliable signers, the recovery-correct validators and two bounds, as Reliability is for density; the standalone safety layer accepts forked histories as execution inputs. CommitSpec.lean is the bridge from any DagRule: a deterministic VM maps each commit to one checkpoint, and a SigningRule states the protocol as two rules, sign what you commit on your own view and witness what you proposed. CommitProofs.lean ties every online correct validator's proposal to a given commit through Properties.Agree, and composes with a Support's Commits law so that production and certification alone yield a finalized checkpoint for a correctly led slot. Hybrid's instance is Integration/HybridCheckpoint.lean: the paper's FlexibleFaults, the hybrid classes plus alive-but-corrupt signers at fabc < n − 3·fb − 2·fc, is one SigningFaults, and at abc = ∅ the online correct validators are a quorum of both the signing threshold and the core reliability. The bridge composes with the schedule mechanism through its own agreement theorems: one Barnacle Run per validator, at any boundary, so the segmented adaptive run too, finalizes what any of them commits in a configuration (Integration/BarnacleCheckpoint.lean, by configAgree). The *Spec.lean files are the human-review trust boundary. CommitSpec.lean also states its theorems as Prop-valued claims, so CommitProofs.lean needs no reading; the safety and recovery pairs still keep theorem statements in their *Proofs.lean files, where the statements, not the bodies, require review. Conditional on those inputs, quorum intersection derives same-height uniqueness and within-epoch prefix consistency; checkpoint safety is intentionally scoped to one epoch. Concrete witness messages prove that finality leaves a recovery-correct recorder. Recovery broadcasts concrete checkpoint-certificate payloads carrying signer sets and checkpoint content. An explicit local verifier checks the epoch, quorum, and every authenticated proposal, with a soundness theorem constructing a CheckpointQC; malformed broadcast inputs are not channel-excluded. Finite highest-checkpoint selection handles the empty case with the closing epoch's canonical execution genesis. Submission and preservation are explicitly scoped to the closing epoch, so retained older records do not make later recovery rounds inconsistent. This recovers checkpoint history under explicit submission, broadcast, validation, and adoption assumptions; it does not recover the discarded DAG or restart consensus. The broadcast algorithm and the paper's post-checkpoint VoteQC extension are not formalized.

• Integration (LeanDag/Integration/): the arcs are proved to compose — not by settling a quadratic matrix, but by naming the invariants each consumes and proving the two universe transformers preserve them, after which a validator running four mechanisms at once still cannot disagree about a verdict (hybrid_agree_stack). The deployment constraints only the composition reveals: garbage collection at lag Λ supports one-message recovery from outages of up to Λ rounds and no more; an adaptive score must read a window of rounds the horizon has not cut, and nothing about the universe that adding blocks changes; and a validator pruned past its own history can read but not produce until it re-genesises — a provision that needs no exemption from the self-parent rule and no agreement on where anyone's cut falls.

• Crash-fault consensus (LeanDag/Nemo/): Nemo-Nemo, the same commit rule at a bare majority quorum — n ≥ 2f + 1, at most f validators halting, none equivocating — proved safe with no fault bound and no side conditions (Nemo.decided_unique): universal non-equivocation retires the twin machinery, and the quorum is consumed exactly once in the agreement proof. Liveness holds at the classical bound (Nemo.all_decided_below_of_fairRun) under a fairness clause the mechanisation sharpens: with no failure detector a lone committed leader settles only the slot two rounds below it, and progress requires committed leaders at adjacent rounds — which round-robin provides by counting.

• Mahi-Mahi (LeanDag/MahiMahi/): the asynchronous protocol (arXiv:2410.08670) — the same rule at a wave of w rounds, votes counted through the causal cone with a canonical support choice — proved safe for every w ≥ 3 (collapsing onto the core at w = 3) and live with no synchrony hypothesis: every wave directly commits some correct validator's block at w ≥ 4, at least n − f − |byzantine| of them at w ≥ 5 (the core's own common-core lemma), and liveness follows from one clause on the schedule and the DAG — the late-revealed leader keeps landing among the committed candidates — which a coin makes true and which synchrony derives from fairness. Two findings about the published argument: the five-round count holds only for non-equivocating authors (1/3 per wave, not 2/3; 2f + 1 leader slots for a deterministic commit, not f + 1), and the core's per-candidate skip rule is weaker than the implementation's slot blame. The arc is built under a statement/proof partition: definitions and statements are the audited surface, proofs are generated, and a checker enforces the split.

• Steelhead (LeanDag/Steelhead/): two rules on one DAG, the core's at ws = 3 and Mahi-Mahi's at wa, every slot given a kind by the schedule and reading the wavelength of that kind, an undecided slot anchoring at its own, r + w(κ). The two are one rule read at two wavelengths: at three Mahi-Mahi's relation is the core's, slot for slot, which is why the arc carries a single family of predicates for the 3f + 1 pair. Verdicts agree across views and routes and across the two rules, a direct commit under one handed over to an anchor decided by the other, at every wavelength function of at least two rounds, which is what the proofs consume. Three is the wave at which the vote-and-certify pattern of the 3f + 1 pair first has a round to put a certificate in: at two the vote round is the slot's own, so no candidate is certified and every slot is directly skipped. Reading the wave at the kind rather than at the round is what leaves the rule banded, so safety and truncation-locality come with it. A witness on data settles why an undecided slot reads the floor at its own wave and not at its anchor's. Live under synchrony at the slot's own wave, by the direct rule, and a slot is decided once every slot from its floor up to a reliably led one is decided. A committed asynchronous slot does not decide the synchronous slots below it: a direct commit reaches a lower slot only through a decided stretch, and at every period k ≥ ws that stretch holds a synchronous slot the adversary keeps undecided, the leader block delivered to exactly f + 1 validators so that neither quorum forms, on data at n = 4. The protocol therefore drives its period from a second verdict, read at the control slots, the coin rounds of each scan, after the reference implementation: the Mahi-Mahi arc at a per-scan sub-schedule under a coin map, agreed per scan, live under Mahi-Mahi's clause with a run of wa control slots, and committing with the counting lemma's probability under a uniform coin (PMF). The period sequence is stated afresh as a relation over fixed intervals and is agreed under any deterministic update rule, so the output at the adaptive wavelength is too, over the intervals the record's own rounds fall in, and so are the ledger of a settled prefix and the slot each block enters at. The output is live under the failover the implementation applies, period 1 at an anchor more than I rounds above the agreed output's last commit: a slot two intervals below an anchored one is decided once a run of wa good coins above it is in view, and over the coins of M blocks of K rounds a validator's scan stalls below the slot or leaves it undecided with probability at most 2 · ((n^K − (n − f − b)^K) / n^K)^(M/2), which vanishes, and over a sequence of records with the coin drawn as a process the slot is decided almost surely, "with probability one" as the paper states it, both against an adversary that builds its record from the draws already made. A crashed leader is skipped, partial dissemination does not defer, an equivocating Byzantine leader at a slot's floor is its anchor and holds it undecided on data, the chain of floors decides the slot it starts from once it reaches a reliably led landing, the round-robin schedule the implementation runs leads three consecutive rounds reliably past every round at n = 3f + 1 and brings the chain to such a landing within n − |T| hops, and within b once the other validators outside the reliable set have crashed, a reliably led slot commits under either execution discipline, the reactive schedule's waits and the timed schedule's rated timeout, a block the reliable validators have referenced is delivered by the first committed slot above, whoever led it, any family of rules whose laws hold composes into one whose laws hold (Steelhead's rule the composite of Mahi-Mahi's at each kind's wave, by definition), Definition 1 holds clause by clause over settled prefixes, and Algorithm 3's replay is data whose selection stays among the candidates, whose window counts the counting lemma's candidates once a quorum has populated it, whose asynchronous term is at most the rule's own value on the same data, whose commit weight is the rule's commit probability on the window, whose probes succeed only on certificate quorums the DAG holds and exist whenever the canary is coprime to the candidate, and which keeps the period in range; on data it recovers from period 1 on a healthy window, keeps its period on a startup window and on a complete window too short for a wave, which the paper's interval bound admits, and answers a stalled period at every anchor of the rotating stall, where no block above round 2 is ever output until the scan's failover hands the period to 1 and a run of the coin decides the stalled slot. The theorems are also stated for any rules meeting the paper's interface, read through the relation's laws and a few clauses (A4's commit under synchrony, a silent leader's skip, a counting floor for the coin), and instantiated twice: at the 3f + 1 pair, whose statements above follow from them, and at BlueBottle's 5f + 1 pair, Odontoceti at the synchronous kind and Async BlueBottle at the asynchronous one, which gets Theorems 1 to 4, the ledger, atomic broadcast, and the coin at the floor n − 3f, the paper's p ≥ (n − 3f) / n. The replay's reading of its window and the timeout appendix count certificates and stay with the 3f + 1 pair. The arc is under the statement/proof partition.

• Async BlueBottle (LeanDag/AsyncBlueBottle/): the asynchronous variant of BB-Core (arXiv:2511.15361, Appendix G) — Odontoceti's two-round arithmetic at a three-round wave, a round-(r+2) block voting through its causal cone with Mahi-Mahi's canonical support — proved safe at n ≥ 5f+1 and live with no synchrony hypothesis under Mahi-Mahi's clause: every populated wave directly commits at least n − 3f correct validators' blocks (the paper's 2f + 1 at the boundary, by a double count at every n), so 3f + 1 leaders per round always include a committed one. Two findings: agreement needs the canonical candidate the paper's Observation 4 assumes away, and the paper's TryDirectDecide is order-dependent under equivocation, which the implementation's slot-level blame avoids — both realised on data, and both already repaired in the paper's current draft.

• Black Marlin (LeanDag/BlackMarlin/): the three-round commit rule of a partially synchronous protocol (DISC 2025) that uses neither reliable broadcast nor a common coin and elects an anchor in every round. Its own safety results hold at the core's committee n ≥ 3f+1, and liveness above the same structural condition as the rest of the development, from a run of two consecutive reliable anchors. Definition 1's Agreement and Total order do not. At n = 4, f = 1 two reliable validators output different twins of an equivocating anchor and neither ever outputs the other's; on the same execution they order two reliable authors' twinless blocks oppositely, which no rule for choosing among twins can repair. The repair that restores both descends to a supported anchor, and no validator can run it: deciding from its own view loses safety, waiting for the evidence loses liveness. The arc is the second under the statement/proof partition.

• Minnow (LeanDag/Minnow/): crs*, the commit rule proposed as minimal for eventual synchrony (arXiv:2608.18029), which decides a leader slot from the round immediately above it — 2f+1 processes pointing commits, 2f+1 not pointing skips. Two of its clauses are written in a way their own sentences do not support, and both are settled on data at four processes with f = 1. Two defects survive either reading. A slot counts as resolved when some vertex of it lies in a candidate's causal past, which is not that vertex being decided: under equivocation one twin carries a later leader past the slot while the other acquires its quorum, costing Safe-Commit — and Lemma 10's own case split is where the paper's proof permits it. The commit and skip thresholds then leave a gap no view ever decides, costing Live-Commit for the rule paired with a multi-leader round robin, though not for the rule alone.

• FinWhale (LeanDag/FinWhale/): a fast path at a tunable committee (arXiv:2606.26292), which commits a leader block one round above it — n − p distinct validators referencing it — at n = 3f + 2p − 1, 1 ≤ p ≤ f, where p is not a second class of fault but how many of the round's votes the path can do without. Its safety rests on one statement: under such a commit every block two rounds up is evidence for it, so no view can commit a conflicting block, skip the slot, or reach a different verdict through an anchor. The committee is exactly the least at which that closes — at one validator fewer the count falls one short, for every f and p in range — which is a tightness result the paper has and does not use, asserting optimality by citation instead. Liveness is derived from the protocol's own block-creation conditions C1, C2 and C3 rather than from reference coverage, which a reactive builder does not have; the two-message-delay latency of Definition 1, stated and not proved there, is proved here. Three further findings: Lemma 22's proof covers p = 1 only, the C3 case of Lemmas 18 and 19 counts one validator too many into a set and has no margin left at p = 1 once that is fixed, and Lemmas 6 and 7 are routed through a clause that a validator which has not seen the committed block satisfies for nothing. A Run bundles one execution and states what a validator guarantees — agreement, total order, integrity, validity — with no verdict assignment, view or well-formedness condition in the statements. And a Mysticeti DAG under this development's denial-of-service condition satisfies FinWhale's validity rule with the self-parent edge included, so the whole arc applies to it unchanged — on the reactive schedule such a universe is a run at every horizon, and the condition provably never leaves a builder short of authors it may cite.

• Barnacle (LeanDag/Barnacle/): the adaptive leader count — every few seconds, measure on the agreed DAG the fraction of leader slots the base protocol decided directly and drive the number of leaders per round with an additive-increase, multiplicative-decrease rule — proved safe and live over an explicit interface rendering the paper's assumptions A1–A4, and instantiated on Mysticeti, Odontoceti, Nemo-Nemo and Orcaella. Safety is agreement of the configuration sequence and of the ledger for any update rule, under no synchrony or fairness hypothesis (Agreement.holds, Ledger.holds): the algorithm decides under the count in force and only then switches, so each configuration's verdicts are derivations against one fixed schedule and no fixpoint is needed. There is no total run — a finite universe closes finitely many configurations — and the paper's sequence of configurations is what every prefix of it agrees on. Liveness is Configuration Progress and runs of every height under a horizon (Progress.holds), from a clause on a schedule the paper assumes of its base protocols and that its own rotation does not meet by this development's run-fairness route at two leaders and four validators; it holds by a descent through the heads of rounds and a pigeonhole on residues (Heads.holds), so each rule is live under round-robin at every leader count — the paper's A4 for its schedule, proved. Seven findings for the paper, among them that its liveness clause needs a margin above the slot and that Nemo-Nemo's slack is what a majority may miss, not the crash bound. The Orcaella instantiation holds at every admissible indirect threshold, over the subtype of universes whose honest — crash-prone included — class does not equivocate, at slack fb + fc and gap n + 1; its witnesses include one DAG the interval's two ends decide differently, the twin-canonicity case at the genuinely mixed committee, and the slack proved exact. The arc is the third under the statement/proof partition.

• Hydrozoan (LeanDag/Hydrozoan/): the dual-path commit rule of the Hydrozoan paper under the hybrid fault model of DagHydrangea — n ≥ 3f + 2c + k + 1, at most f Byzantine, at most c crashed, k a tunable slack — which commits a leader in two message delays on n − p votes, p = ⌊(c + k)/2⌋, or in three on 2f + c + 1 certificates, skips it on n − p blames, and decides a slot none of those settles from the nearest committed anchor by a graded rule (certificate, weak quorum, skip). Safety is agreement of any two verdicts across views and routes, from six threshold inequalities that hold for every fault configuration the class admits — no cap on the slack is needed, though the Hydrangea paper states one — and prefix consistency of the committed sequences, and of the delivered sequence — the ledger filtered through the linearizer's persistent set, for any deduplication key — with Integrity: no key delivered twice. Validity closes the four properties of atomic broadcast: from the round of synchrony on, every block of the synchronised correct set is delivered. Liveness above a structural rendering of synchrony routes through the slow path, the only one a quorum of correct replicas is sure to reach; the fast path and the direct skip are stated as performance facts outside the liveness claim, firing exactly when the actual faults fit p. The hypotheses are grounded by exhibition: the wave-aligned rotation is fair with no premise, where per-slot rotation is starved inside the hybrid bound, and the synchrony package is realizable at every horizon. Two findings for the paper: the anchor-sees-the-fast-footprint row is consumed in a strengthened, non-Byzantine form, and a slot can fast-commit while no certificate for it exists anywhere, so the indirect rule's weak rung is necessary. The arc is the fourth under the statement/proof partition, and the one that partition was designed for; it is developed in asonnino/mysticeti beside the reference implementation.

• Optimal-Hydrozoan (LeanDag/OptimalHydrozoan/): the theory-only variant of Hydrozoan whose fast path tolerates one more fault — pOpt = ⌊(c + k)/2⌋ + 1, Hydrangea's lower bound on two-round commits, at the same committee — by FinWhale's device: a decision-round block that has seen the leader equivocate must not reference the leader's block, and quorums of decision-round blocks that are fast evidence for a candidate replace Hydrozoan's weak quorum of votes, in the indirect rule's second rung and in the direct skip. The seam consumes the validity rule exactly once, so the evidence rung is unique with no tie-break and the statements need no order on ids. Safety and liveness mirror Hydrozoan's; what the arc adds is that a slot whose leader produced no candidate is skipped by the guaranteed quorum alone — a liveness claim where Hydrozoan's skip is opportunistic — and not otherwise, since with a candidate present f Byzantine votes defeat the skip, FinWhale's attack on data. At k = 2f + c − 2 every fault fits the fast path at n ≥ 5f + 3c − 1. A peer arc importing the Hydrozoan arc read-only, and the second developed in asonnino/mysticeti.

• Bluestreak (LeanDag/Bluestreak/): the sparse uncertified DAG (IACR ePrint 2026/898), whose non-leader blocks carry two references and whose round-r+2 blocks claim the leader certified — by a field, or for a leader block by the votes it carries — with the n − f votes backing a claim outside the claiming block's causal history. The rule is the core's with claims for certificates, proved safe at n ≥ 3f+1 under the trace the protocol's referenceability discipline leaves on the record: every claim an honest block reaches is certified (Bluestreak.bluestreakLaws). Stating it took one field more of the anchored relation — what a committed anchor is known to be — because the rule's own laws fail of an uncommitted anchor, on data; and its per-candidate skip is strictly stronger than the core's slot blame, on data. Liveness is stated on claims, not references, and the pull pacemaker is a reactive schedule whose referencing discipline is exactly the invariant safety assumes (Bluestreak.ReactiveB.disciplined): every reliable validator decides a reliable-led slot on its own view (Bluestreak.ReactiveB.decided_local), and a sparse DAG grown to every horizon witnesses the schedule. The arc shows the five properties over the disciplined records, the block format being assumed of certified blocks rather than checked per slot, since a validity predicate cannot read which slot a block sits in; the band's novelty clause then reads the anchor, because a claim names its candidate where every other rule's evidence references it. Chain quality does not apply to a two-reference block. And garbage collection is a protocol question here: referenceability asks that every claim in a block's history be provable, which a validator that prunes cannot do, so the rule must be read bounded — two rounds, a claim's reach — and the cut then forgets the claims it orphans.

Every definition is exercised on concrete models by decide before anything is proved from it, and every principal result depends on exactly Lean's three standard axioms (propext, Classical.choice, Quot.sound) — no sorry, no bespoke axioms, no native_decide.

Building

lake build

Requires elan. The toolchain version is pinned in lean-toolchain; lake build will fetch it automatically.

A Makefile splits the work by what it costs. make fast builds the library alone and runs the checks that cost nothing, which is the loop to work in; make check adds the concrete-model layer and is what a commit needs; make deps regenerates the dependency graph and is only needed when the set of declarations changes. make help lists them.

Layout

Four kinds of arc. Each directory under LeanDag/ is one of them, and its entry file says which:

Common/ is the substrate all four read; Properties/ is the contract a commit rule meets and the other three consume; Integration/ is what pairs two kinds at once — a schedule over a rule, or two transforms composed. A commit rule reads in four parts, and its files are named for them: the universe and the rule under Model/, what it shows in Properties.lean or Carrier.lean, and what it earns in Record.lean.

• LeanDag/ — theorem/definition source: the core DAG and Mysticeti development at the top level, with the pacing structures in Mysticeti/ViewPace.lean and the delivery layer they induce in Mysticeti/PaceDelivery.lean. Common/ (twenty files) holds what every rule shares: BlockRecord.lean is the one universe shape every rule instantiates, with the generic cut, fill and re-genesis built against it once; Causality.lean and Participation.lean hold the fault-agnostic vocabulary — reachability, the finite cone, production and coverage — stated over the raw block data beneath it; Anchored/, Support.lean, Rules.lean and Ledger.lean hold the generic anchored-rule interface, the counting arguments a support discharges, the five rule combinators, and the ledger a decided sequence assembles into. Properties/ states the target properties themselves (DagRule, Agree, Commit, Band, Sustain, Truncate, …) and the generic mechanism theorems every carrier gets for free (Properties/Arcs/); Timed/ holds the timed model built on top — coverage, and the bridge from synchrony into certification — kept apart from Properties/ since it is timing-specific (scripts/check-arc-holes.py enforces the separation). The arcs are in subdirectories (Quality/ — chain quality; DoS/ — equivocation and the novelty budget; GC/ — garbage collection; Odontoceti/ — the two-round protocol; Reactive/ — the reactive schedule; SafeSkip/ — crash recovery in one message; Adaptive/ — adaptive leader schedules, a reputation score over Barnacle/'s run; Hybrid/ — Byzantine and crash faults apart; Nemo/ — crash-fault consensus at a majority quorum; Minnow/ — the minimal commit rule and its counterexamples; FinWhale/ — the fast path at n = 3f + 2p − 1, whose Model/ holds every definition of the protocol and no proof; MahiMahi/ — the asynchronous rule at wave w, AsyncBlueBottle/ — the two-round rule at a three-round wave, BlackMarlin/ — the three-round rule with an anchor every round, and Barnacle/ — the adaptive leader count over an interface for the four base rules, Hydrozoan/ — the dual-path rule under hybrid faults, with its own fault model and universe, and OptimalHydrozoan/ — its fast path at Hydrangea's bound, a peer arc importing the first, and Steelhead/ — two rules at one wavelength function, with the chain verdict, all under a statement/proof partition (Model/, <Result>/Statement.lean, <Result>/Proof.lean); Network/ — the composed denial-of-service capstones; Integration/ — how the arcs compose).
• LeanDag.lean — root import file.
• LeanDagTest/ — decide witnesses and concrete models, mirroring the same layout.
• docs/ — the design records and the report. docs/build-pdf.sh compiles them to docs/pdf/ — requires pandoc and typst (brew install pandoc typst).
• scripts/ — the extraction and verification pipeline. DepGraph.lean and depgraph.py extract and draw the support diagrams (docs/depgraph/README.md); svg2pdf.sh renders them to PDF; extract-decls.py reads every declaration with its docstring and statement into docs/decls.json, and gen-reference.py regenerates the report's reference appendices from it, selecting the declarations the body and the statement index name; audit-report.py checks the report's cross-references, its Lean identifiers, and every displayed statement verbatim against the compiled source. docs/decls.json and docs/depgraph/deps.tsv are extracted, not tracked; a fresh clone builds, then runs the two extractors before the audits. Regeneration is deterministic, so regenerate-and-diff is the pre-merge check. check-arc-holes.py enforces the statement/proof partition of the arcs that adopt it; audit-rounds.py closes each protocol's decision relation over the dependency graph and checks that no rule reads an absolute round, which is what the offset band needs (docs/target-properties.md §3.4c); audit-conformance.py recomputes which protocols have shown which properties (§11.2); and black-marlin-figure.py draws the execution that refutes Agreement (docs/figures/).

Documents

Contributors

• Alberto Sonnino — the crash-fault arc (LeanDag/Nemo/, #1): the majority-quorum foundation and its intersection lemma, the wave-two commit rule, agreement without side conditions, liveness at n ≥ 2f+1, and the three-validator witness model. He also contributed the wave-robin schedule (#3), the Mahi-Mahi arc (#5), the Barnacle arc (#7), and the Hydrozoan arc (LeanDag/Hydrozoan/, #8): the dual-path commit rule under hybrid faults, its safety from the threshold table alone and its liveness through the slow path — and its Optimal variant (LeanDag/OptimalHydrozoan/, #9), the fast path at Hydrangea's bound.

• Lefteris Kokoris-Kogias — the resilient checkpoint arc (LeanDag/Checkpoint/, #4): the assume-guarantee model of epoch-bearing proposals over append-only validator state, same-height uniqueness and within-epoch prefix consistency from quorum intersection at fabc < n − 3·fb − 2·fc, resilient finality, and highest-checkpoint recovery with its local verifier and soundness theorem.

License

MIT — see LICENSE.