GitHub repository makechain-v2 ↗

Formal verification plan

Draft protocolSource at 169cbd2 ↗Source SHA-256 a3fc03f…698
Status
Decision D48, accepted by the repository owner on 2026-09-23 (owner record (external site)), superseded in part by decision D49 (TLC pin, trace point, Lean role, just check-formal); extended by decision D50 (MC-04, the MC-02 export installation extension, and the non-goals of section 9), accepted by the repository owner on 2026-09-25
Specification
Revision 15 (spec/SPECIFICATION.md SHA-256 5fdadd0efc60fb97a443403c61706acfb5ee4686056a3b054221185143af24da)
Baseline
dd007e2
Tools
TLC stable v1.7.4 (2.19, rev 5a47802), Lean v4.31.0 (one pin for formal/lean and formal/aeneas, equal to Aeneas's); digests in formal/tools/pins.toml. Each formal/check.sh run prints the TLC jar digest, the Lean version line, commit and toolchain manifest digest, and fails on a jar digest or Lean commit that differs from the pins; the Lean manifest is compared with its pin on Linux x86_64 only, and elsewhere Lean is checked by commit

This plan extends validation section 7.1, which already selects TLA+ and TLC for MC-01 to MC-03 (decision D31). It adds three things the current plan does not have: implementation linkage through trace validation, Lean 4 proofs that are not bounded, and a staged path from Lean models to proofs about the Rust code itself. It changes one gate requirement, by owner decision (D48): an MC gate's implementation linkage also includes checking recorded executor traces against the model, in addition to the model-to-implementation replay validation 7.1 already required. Nothing else a gate requires changes.

1. Scope

The specification treats consensus as a trusted component: Simplex, marshal, glue, and the database set order, finalize, and persist opaque blocks (R-18.34). The risk Makechain owns lies above that line, so this plan verifies:

Area Invariants Gate Tool
Authority lifecycle and accounting INV-STATE-01..05, -08, -09; INV-AUTH-02..04, -07, -09 MC-01 TLA+, Lean
Projects, roles, usernames, slugs INV-STATE-09, -10; INV-AUTH-04, -05, -10 MC-01 TLA+
Settlement import and trust deadlines INV-SETTLE-01..08 (-07 structurally) MC-01 TLA+
Release and validator schedule INV-GOV-01..10, -12 MC-03 TLA+, Lean for active_release(h)
Canonical encoding R-6.1, INV-CONS-05, -06; encoding.md registries none today Lean
Consensus-to-execution lifecycle R-12.10, R-12.11, R-12.14, R-12.22 to R-12.24, R-12.29 e; INV-CONS-01, INV-FAULT-01 MC-04 (planned) TLA+

Out of scope: Simplex itself; cryptography (assumed: signatures unforgeable, hashes collision-resistant); availability and performance. MC-02 (genesis and crash recovery) was added to the scope on 2026-09-23 and is modelled in formal/tla/mc02. MC-04 (the lifecycle between Simplex, marshal, glue and the Makechain adapter) and the MC-02 export installation extension were added on 2026-09-25 under D50; both are planned and unwritten (sections 7 and 8), and section 9 lists what stays out of scope.

Commonware ships a Quint model of Minimmit, not of Simplex, and NyxFoundation's simplex-fv proves the Simplex paper's safety and liveness in Lean. Neither is a dependency of this plan. A model of Simplex as Makechain configures it stays unscheduled: MC-04 consumes Simplex only as quorum counting over certificates and cites the Deferred vote gating to source (contract K13), so such a model would add assurance only for a configuration the paper's model does not cover, and none is planned.

2. Layers

Layer 1: bounded models (TLA+, TLC). One module per gate slice under formal/tla/. Each campaign runs: a complete safety search inside declared bounds; reachability witnesses for every success, rejection, and exhaustion path (validation 7.1 nonvacuity); and mutation runs, each breaking one rule, which must all be caught. Fast bounds go into the local gate; deeper bounds run by hand.

Layer 2: trace validation. Two directions. Validation 7.1 already requires the second ("representative successful, rejected, and recovery traces replayed against the real implementation"); D48 adds the first:

  • Implementation to model. Execution runs inside glue's Stateful actor in propose, verify and apply, including speculatively, and a proposer skips a failed candidate so that it never enters a block (state-machine.md section 1, R-8.14). Under decision D49 the trace contract is the design record docs/execution/design/vp-02-trace-emission.md: records are a permanent part of the ExecuteOrderedBlock outcome (one step record per candidate attempted, plus one end record per block), never behind a cargo feature; the post-state is read back through the real member databases by the makechain-trace abstraction, never supplied by the executor; offline deterministic replay is the primary driver, and under glue::simulate the records of every verify, propose and apply are compared with the offline records. Finalized blocks contain only accepted commands, so rejection evidence comes from generator-driven proposal-mode runs and invalid-block verify runs. A Trace<Model>.tla module reads the newline-delimited JSON and constrains Next to follow it, so TLC checks that every recorded step is a model step and that every observed state satisfies the invariants. This is the technique of Cirstea, Kuppe, Loillier, and Merz (SEFM 2024), which reported discrepancies between specification and code in each system it examined.
  • Model to implementation. TLC counterexamples and witness traces are exported as the same JSON and replayed against the executor by a Rust test harness. Every witness becomes a positive regression test; every counterexample becomes a permanent negative one (validation 7.1).

The harness needs no second model checker, only Python 3 for the converters: each NDJSON trace is converted into a generated TLA+ module that the trace specification reads, and TLC's text error traces are parsed back for replay, so it runs on the pinned TLC alone (TLA+ CommunityModules, the usual JSON reader, does not load on TLC 1.7.4).

Layer 3: Lean models (unbounded). Executable Lean 4 definitions of the same rules, with theorems for all sizes and values. They complement TLC: TLC finds counterexamples quickly inside small bounds, while Lean proves the rule holds without bounds. formal/lean uses core Lean only (no Mathlib), so its trusted base is Lean's kernel. The gate replays every Makechain module through the kernel with leanchecker, so a declaration added by meta code that skipped kernel checking (debug.skipKernelTC with addDecl) fails it. It then walks every constant of every Makechain module, internal names included, and rejects any axiom other than propext, Classical.choice and Quot.sound and any declared axiom or opaque constant. In the sources under formal/lean/Makechain, with comments and string contents removed, it rejects the words sorry, admit, axiom, opaque, implemented_by, extern, native_decide, unsafe, partial and decide +native, any import Lean or import Lean.*, any set_option debug., addDecl, admitGoal (so Lean.Elab.admitGoal), and the private modifier. The source scan is defence in depth: a spelling it does not match still fails the gate through the kernel replay.

Layer 4: code-level proofs (Aeneas). Pure functions are translated from Rust MIR to Lean by Charon and Aeneas and proved equal to the Layer 3 models, which formal/aeneas/lean imports from formal/lean by a Lake path dependency. There is one Lean toolchain pin for both layers, and it follows Aeneas's own pin (v4.31.0 today). Layer 4 has its own trusted base, stated explicitly: Lean's kernel, Mathlib (which the Aeneas library imports) and the Aeneas Lean library (its models of machine integers, arrays, slices, iterators and loops), plus Charon and Aeneas themselves and any hand-written model of a standard-library function the library lacks. None of that enters Layer 3's own theorems. Aeneas handles safe no_std code with checked arithmetic, which fits AGENTS.md rules 15 to 18, but it needs hand-written Lean models of the alloc collections Makechain uses (BTreeMap, BTreeSet, Vec) and does not accept every loop shape. Candidates, in order: Amount256::checked_add, checked_sub, checked_mul; tag_enum! decode classification; bounded scans; then the executor's ledger and keychain transitions.

3. Delivered in this change

Item Result
formal/tla/mc01 (MC-01 slice A) complete search, 364,422 distinct states; 17 of 17 witnesses reached, including rejections by max_charge alone, by a moved expected generation (reclaim and revoke-one), by a moved expected delegation epoch (revoke-all), and of a push signed under a superseded authorization_generation; 22 mutations, 21 each caught by its named property (replay, stale epoch, stale signed generation, replacing a usable key, max_charge, the revoke-all table guard, both KEY_REVOKE bindings, allocation of revisions and incarnations, including KEY_AUTHORIZE reusing next) and import_nonstrict required to pass because the strict-advance import is a trusted input here (checked in slice C). Eight properties restate or stay close to their guards or effects, and the README lists them, including MarksMonotone, the only catcher of revoke_all_resets_marks; DepositStepExact catches the two expected-generation mutations through the ghost record of the signed generation, and AuthorityLossIsAuthorized catches reclaim_live and authorize_live through the step label, as the README says; set_keeps_revision is caught by the ghost-history consequence SupersededRevisionNeverMatches. The ref compare-and-set value of R-8.15 only gates a step and no property checks it, so INV-STATE-03 for refs is checked on the allocation side only (README, "Known gaps"). Not modelled: signer vectors (R-7.31), keychain_revision, metering, and the expected generations of KEY_AUTHORIZE. Reject atomicity is assumed by construction; amounts are unbounded naturals
formal/tla/mc01b (MC-01 slice B, FV-01) four fast configurations (P, R, U, and S with projects and usernames on one ledger, two prices and a real strict-advance import), complete search; re-freeze while FROZEN per the section 8.4 table; 30 of 30 witnesses reached, the cooldown and allocation-counter rejections read ENABLED of the claim action (U has the credit for a claim to be refused by exhaustion, not by solvency); 24 of 24 mutations each caught by its named property. Eight properties restate a guard or effect and are labelled, six of them the only catcher of their mutations. "No stale authority resurrection" is argued, not checked: signed compare-and-set values only gate steps, only the control and grant generations and the username guards and counter are checked by a (restating) ghost property, and ten other signed guards can be dropped with no property failing (README, "Known gaps"). Reject atomicity is assumed by construction
formal/tla/mc03 (MC-03, FV-03) both profiles, B = 2 and B = 3 (the latter with MinDelay = 3), and a five-key validator-set configuration, complete search; a second node restarts from a checkpoint holding exactly the fields its outputs read, minus the players, which it recomputes from the schedule (R-13.20); RestoredStateExact checks that the restored state equals the first node's, and the replica properties (ReplicaVerdictsAgree, ReplicaInstallersAgree, ReplicaEpochInfoAgree, RulesFromParent) follow from it and gain content only against mutations, as the README says; fields no output reads are not modelled; cutoffs checked as consequences (LockInFromParent, CriticalFixedAtLock, ActivationNotEarly), including CANCEL and DEFER in the lock block, with the remaining guard restatements labelled; conditional liveness holds under stated fairness, and a departing validator's non-cooperation rests on section 13.3's quorum sizing, not on the model; 35 of 35 witnesses reached, including a fixed-profile append rejected only for the profile and a validator cancel accepted in the last eligible block under B = 3; 39 mutation runs (31 mutations: the distinct names in the model's Mutation domain; eight run under two configurations) each caught by its named property. Not modelled: paged checkpoints, a checkpoint older than the rejoin point, late-joiner floors, anchor age, two commands per block
formal/tla/mc01c (MC-01 slice C, FV-02) two configurations, complete search (224,940 and 26,192 distinct states); 29 of 29 witnesses reached, the two deadline-term witnesses from a checkpoint a forward step wrote; 28 of 28 mutations caught by their named property, including one caught only by DeadlineCheckedFirst (trust deadline evaluated before authentication), an installer accepted_at taken from the descriptor between the previous value and the block time (caught only by AcceptedAtIsBlockTime), a refresh that never moves the checkpoint (caught only by RefreshMovesCheckpoint), and two contract-replacement mutations run under GenMax = 2, with WC_PredecessorRejected requiring a proved predecessor contract (not reached when predecessor proofs are accepted). Two properties restate a guard's threshold from the rejection side, and CheckpointAdvances, NoMonetaryEffect, RefreshMovesCheckpoint and AcceptedAtIsBlockTime restate a guard, frame or effect, as the README says. Crash, restart and recovery are excluded (MC-02)
formal/tla/mc02 (MC-02) four submodels (genesis, node, export, fence; export is checked as exporter and consumer, so five safety configurations), complete search; custody and the identity-safety WAL on separate volumes, with fence steps 3 and 4 split per operations 2.4; rebootstrap repeatable; conditional liveness under named fairness, with operator and environment steps listed separately; the successor refuses a restored journal below the recorded ceiling (P-32 records when that ceiling is taken); 40 of 40 witnesses reached, including a consumer redelivery that the EventId dedup leaves without effect; NoSkippedHeight counts only heights not rolled back by a restart; 38 mutations in 40 runs, each caught by its named property alone, and the ten caught only by a restatement (six) or a ghost property (four) labelled and gap-checked by a manual GAPS=1 run (not part of the gate); every assumed Commonware behaviour is either cited to a v2026.9.0 source line (contracts K1 to K12, and the README's source citation that an empty keyless batch appends a commit) or listed as a reading: reading 10 (the ghost base kept across a sync), which no Commonware source supports
formal/trace (FV-05, FV-06 prototype) both directions run against ref-ledger: six seeded 400-command traces validate; nine incomplete or tampered traces are rejected; eighteen witness traces replay without divergence, and a rejected probe must leave the state unchanged; truncated TLC traces are refused; seventeen injected executor bugs, each detected in both directions. ref-ledger transliterates the model, so this demonstrates the harness, not implementation linkage
formal/aeneas (FV-07) Charon 0.1.270 and Aeneas pinned; checked_add, checked_sub, and checked_mul, each translated from the crate as it stands, are proved for all inputs never to panic and to equal Amount.lean's checkedAdd/checkedSub/checkedMul (hence the checked-arithmetic specification). The previous checked_mul did not translate ("Could not match the contexts"), so SB-00 adopted in amount.rs the behaviour-preserving rewrite that also meets AGENTS.md rules 15 to 18, refreshed the FB-09, FB-10, FB-11 and SB-01 evidence that pins the digest of amount.rs, and keeps the previous body as a differential oracle in tests/protocol-differential/tests/amount_mul_differential.rs; formal/aeneas/check.sh now extracts and proves all three functions from the one crate. Every theorem uses only Lean's three standard axioms; the hand-written externals of formal/aeneas/lean/Extracted/FunsExternal.lean are trusted
formal/lean/Makechain/Varint.lean decode_encode, decode_canonical, encoding_unique, feed_no_underflow for every width
formal/lean/Makechain/Ledger.lean exec_good (R-9.35), exec_solvent (INV-STATE-01), exec_atomic (R-8.17, definitional), exec_cumulatives_monotone, discharge_unlock_only, discharge_once, discharge_guard_holds, and for INV-STATE-08 exec_counter_monotone, lock_allocates, discharge_retires, discharged_never_relocked. Amounts are unbounded Nat; R-9.35's premise holds by construction
formal/lean/Makechain/{Fixed,Amount,Tag}.lean (FV-04) fixed-width codec canonicity and the u64::MAX rejection table; Amount256 checked arithmetic, modelled loop by loop, equals checked Nat arithmetic; tag classification total and disjoint
formal/lean/Makechain/Release.lean (FV-04) apply_preserves_past, active_monotone, apply_wellFormed, cancel_removes, locked_at_lock_block, unlocked_before_lock_block, cancel_invalid_in_lock_block, defer_invalid_in_lock_block, reach_cancelled_never_active: no valid operation revises an executed height, the active release only moves forward, a critical entry is locked from its lock block act − B − 1 (and not at act − B − 2) so CANCEL and DEFER are rejected there, and a cancelled entry's identity is never active again (R-18.12). locked_blocks_all restates the definition. INV-GOV-07 holds only by the signature of active_release, and is not proved
Axiom audit every headline theorem uses only propext, Classical.choice, Quot.sound

Slices B, MC-03 and FV-04 were each built by one agent, attacked by an independent reviewer that had to cite specification text or a rerun for every finding, and fixed. The reviews found seven blocking defects in the first drafts (missing username lease guards, no property for the section 8.4 authority table, properties that restated guards, bounds too small to exercise R-13.15 b, no property for R-13.12 or R-18.14, and an unproved link from scalar types to the u64::MAX policy). Each model defect has a property and a mutation that the property catches, and the Lean scalar-link defect is closed by a theorem; several of those properties restate the guard they check rather than a consequence of it (for example FrozenBlocksGrant, HorizonRespected, ReservationRespected in slice B); each README labels them, and lists the guards no property checks under "Known gaps".

Findings:

  1. The varint proof confirms the pinned Commonware decoder's claim that every u32 count has exactly one accepted encoding, and that its checked_sub(..).unwrap() cannot panic. The count prefix of a collection therefore has one encoding; the framing as a whole also depends on the element decoders, which this proof does not cover.
  2. Writing the model showed that no indexed invariant says RECLAIM never removes live authority. Section 7.6 states it in prose ("Physical deletion by RECLAIM removes no live authority") and R-9.43 and R-9.47 enforce it, but INV-STATE-04 covers only the converse, that expired records grant nothing. The model checks the obligation as AuthorityLossIsAuthorized, and the reclaim_live mutation shows that no other property would catch its loss. The specification owner may want to index it.
  3. Open specification questions from the slices, recorded with the reading each model takes and a recommended rule text in spec-revision-15-proposal.md (external site) (P-02 to P-16; finding 2 is P-01):
    • R-8.67 keeps a last selected name for the username cooldown, but AccountUsername in encoding.md section 6 has no field for it.
    • encoding.md makes USERNAME_CLAIM.Rename.expected_allocation_counter mandatory, while R-8.64 and state-machine section 6 require the counter only for a claim by a new owner or a fresh claim.
    • An Absent lease guard can become valid again after a name is claimed by another account and reclaimed, while the signer's allocation counter has not moved.
    • The starting revision of a new UsernameLease incarnation is not pinned.
    • PROJECT_SET_STATUS to the current status, and a maintainer revoking a stale writer grant (section 8.4 table against R-8.47), are unspecified.
    • Whether a key reserved by a cancelled validator-set entry may be re-added (R-13.14 read with encoding.md's cancel semantics).
    • Which semantic scalars reject u64::MAX: encoding.md section 1's row for TimestampMs and the other 8-byte scalars says only "reject u64::MAX where revision 4 requires a reset/end", a conditional that enumerates no types, and the RulesetId row has no rejection clause; the crate rejects it for the counter-like scalars and allows it for TimestampMs and RulesetId (P-15).

4. Roadmap

Step Deliverable Depends on
FV-01 Done (first draft): MC-01 slice B, formal/tla/mc01b owner answers to finding 3
FV-02 Done (first draft): MC-01 slice C, formal/tla/mc01c owner answers to its README's readings
FV-03 Done (first draft): MC-03, formal/tla/mc03 owner answers to finding 3
FV-04 Done: Fixed, Amount, Tag, and Release (active_release(h), R-18.12, the lock block; INV-GOV-07 only by signature) none
FV-05 Prototype done in formal/trace; real linkage waits for the executor to emit the same schema, including the end record makechain-execution exists (IP-04)
FV-06 Prototype done in formal/trace FV-05
FV-07 Done: checked_add, checked_sub, and checked_mul proved in formal/aeneas against the crate; the checked_mul rewrite is adopted in amount.rs by SB-00, with the repository owner reviewing the diff and the evidence of FB-09, FB-10, FB-11 and SB-01 refreshed (section 6) SB-00
FV-08 Aeneas proofs of executor ledger and keychain transitions against Ledger.lean FV-07, IP-04
FV-09 Planned: MC-04 lifecycle model with its trace binding (section 7; framework task VP-10) VP-07, SB-14
FV-10 Planned: MC-02 export installation and standby extension (section 8; framework task VP-11) MC-02; before IP-06C

Each step is written as a brief in docs/execution/briefs/ by the orchestrator, from the framework template, under D48 and D49.

5. Decision

D48 (accepted 2026-09-23). Formal verification uses TLA+ with TLC for the MC gates, with trace validation in both directions as their implementation linkage: model witnesses and counterexamples replayed against the executor, as validation 7.1 already required, and, as a new requirement of this decision, finalized-apply executor traces checked against the model by TLC; Lean 4 (core only, no Mathlib) for unbounded proofs of the same rules and of canonical encodings; and Aeneas for code-level proofs once the executor exists, starting with a pilot. Consensus stays trusted under R-18.34. Tools are pinned by digest in formal/tools/pins.toml. Formal work lives under formal/. A model or proof is qualification evidence only with a reviewer verdict and implementation linkage.

"Core only" applies to formal/lean. The Aeneas pilot's Lean project, formal/aeneas/lean, depends on Mathlib and the Aeneas library, and that trusted base stays inside it.

6. Owner decisions

Made on 2026-09-23:

  1. A just check-formal recipe (D49's name for D48's just formal) runs formal/check.sh, outside check-all. SB-00 adds it: the Justfile digest is pinned by the FB-02 and FB-12 evidence manifests, so the edit needs cargo +1.95.0 xtask refresh-evidence for both FB-02 and FB-12 (FB-12 pins the Justfile and fb-02.json) by the orchestrator in the same change.
  2. D48 is recorded in docs/DESIGN-CODE-ARCHITECTURE-PLAN.md, and validation sections 7.1 and 10 name the trace-validation and Lean evidence entries and the DRAFT MODEL status.
  3. The specification questions of section 3 go to a revision-15 proposal, spec-revision-15-proposal.md (external site), for the owner to accept or reject; spec/ itself is unchanged.
  4. Next work: the trace-validation harness (FV-05, FV-06), MC-01 slice C (FV-02), MC-02, and an Aeneas pilot on Amount256 (FV-07).

Recorded on 2026-09-23, after the pilot: the single Lean toolchain and checked_mul were "left to Claude to decide the long-term correct option" (owner record). Accordingly, formal/lean moved to Aeneas's Lean v4.31.0, pinned once in formal/tools/pins.toml, and formal/aeneas imports the Layer 3 models instead of copying them. The checked_mul rewrite is adopted in amount.rs by SB-00, with the repository owner reviewing the diff: checked_add, checked_sub, and checked_mul are extracted from the crate as it stands and proved in formal/aeneas, and SB-00 refreshes the evidence of FB-09, FB-10, FB-11 and SB-01, which pin the digest of amount.rs.

The Aeneas route past the pilot is accepted as part of D48 (owner record: "Lean 4 staged: spec models first, then Aeneas proofs about the Rust code"); FV-08 is its next step.

Still open: briefs under docs/execution/briefs/ for work executed through the SB framework.

7. MC-04: consensus-to-execution lifecycle (planned)

Status: planned under D50, not written; no TLA+ module exists. MC-04 checks the wiring in which the specification assigns the adapter duties that glue cannot perform: the canonical state_root in verify and apply (R-12.11; glue compares only the ops target, contract K14), None rather than a fatal stop for an uncertified ancestor that does not execute (R-12.23, R-12.24; contract K16), and readiness only when the canonical root equals the header (R-12.29 e). It is small by design: it has no crash-cut granularity (MC-02 owns that) and no execution values (execution is the abstract function Exec(parent, block)).

Constants. Four validators (f = 1) under two configurations: Byzantine-proposer, where one validator proposes blocks of any kind and votes arbitrarily, and crash-only, where every validator is honest and may crash. Heights 1 to 3, views 1 to 4. Each height has candidate blocks of kind good, badCmd (a command fails, R-12.8), badCanonRoot (canonical state_root wrong, ops target correct), or badOps (ops target wrong). A future flag keeps a block's verification pending until Tick passes its time (R-12.22 transient inability). MaxCrashes bounds crashes and MaxFailed bounds the views that end in Nullify (see Liveness).

Variables. tree (parent, height, view, kind per block); notar[v], fin[v], nullify[v] (votes, with certificates derived at 2f + 1); chain, the one global finalized chain that Simplex agreement (contract K19) lets the model keep; avail[v]; verdict[v][b] in {none, pending, valid, invalid}, volatile; pend[v], cached parent state with provenance propose | verify | replay, volatile; applied[v]; dur[v], the durable prefix, taken from MC-02 as an assumption; mode[v] in {crashed, recovering, ready, fatal}, where a node starts in recovering and only ready proposes or votes; failed, the count of views ended by Nullify; time.

Actions.

Action Meaning Rules
Propose an honest leader proposes good on its pending parent state; a Byzantine leader proposes any kind R-12.9
Disseminate a block becomes available to a validator contract K13
NotarizeVote requires availability and a context match only, no verdict contract K13
VerifyStart, VerifyDone Exec yields valid or invalid; a future block stays pending until Tick R-12.10, R-12.11, R-12.22
CancelRetry the wrapper drops or retries a verification; nothing durable changes R-12.22, contract K17
LazyReplay an uncertified ancestor is replayed through apply; badCmd or badCanonRoot returns None, which rejects every dependent R-12.23, contract K16
FinalizeVote requires a notarization certificate for the block and verdict = valid contract K13
Nullify a view ends without a notarization contract K13
Finalize 2f + 1 finalize votes extend chain contracts K13, K19
ApplyFinalized applies the winner from cache or by reconstruction; a failure is fatal R-12.24, contract K15
Crash drops pend, verdict and in-flight work contract K17
Restart reconciles to dur per MC-02 contract K3; ready only when the roots equal the header R-12.29 e
FatalLocal, Tick local corruption stops the node; time advances R-12.14

Invariants. Following the MC-01 and MC-02 convention, a property that restates the guard of the action it constrains is labelled a restatement: it gains content only against mutations.

Property Kind Requirement
NoInvalidFinalized consequence with at most f Byzantine validators, no badCmd, badCanonRoot or badOps block enters chain (R-12.8, R-12.10, R-12.11)
ExecDeterministic definitional, with content only against nondeterministic_exec equal (parent, block) gives every honest validator equal verdicts and equal applied roots (INV-CONS-01)
FinalizeVoteOnlyValid restatement of FinalizeVote an honest finalize vote names a notarized block this validator verified valid, so pending and invalid never yield one (contract K13, R-12.14, INV-FAULT-01)
ReadyOnlyOnRootMatch restatement of Restart a node enters ready only when its canonical state_root equals the header's at the reconciled anchor (R-12.29 e)
NoVoteBeforeReady restatement of the vote guards no vote of any kind while mode is not ready, which covers crashed, recovering and fatal (R-12.29, INV-FAULT-01)
NoEffectBeforeFinalize restatement of ApplyFinalized dur changes only through ApplyFinalized (R-12.22, R-12.23)
ReplayIsNotVerdict restatement of LazyReplay LazyReplay never sets a verdict (glue/src/stateful/mod.rs:87-88)
ByzantineAncestorNeverFatal consequence replaying a Byzantine uncertified ancestor never makes an honest node fatal (R-12.23, R-12.24)
FinalizedWinnerReconstructs consequence an honest node always reconstructs a block of chain (R-12.24)

Liveness. Assume honest leaders occur infinitely often; crashes are bounded by a constant MaxCrashes; failed views are bounded by a budget MaxFailed of at most the view bound less the heights (with four views and three heights, MaxFailed = 1, so the Byzantine leader's view can end in Nullify), so views 1 to 4 cannot be exhausted; every pending verification eventually resolves; and Propose, Disseminate, NotarizeVote, VerifyStart, VerifyDone, LazyReplay, FinalizeVote, Nullify, Finalize, ApplyFinalized, Tick and a Restart that reaches ready are weakly fair. Then the finalized height reaches its maximum. Nonvacuity follows MC-02: a reachability witness for every action and verdict class, and the liveness property must fail when any one fairness assumption is dropped.

Mutations, each with its intended catcher: skip_canon_root_verify and skip_canon_root_apply (NoInvalidFinalized; the apply case needs a child built on a badCanonRoot ancestor that was never certified), pending_as_valid (FinalizeVoteOnlyValid), fatal_on_invalid_ancestor (ByzantineAncestorNeverFatal), finalize_before_verify (FinalizeVoteOnlyValid), vote_before_ready (NoVoteBeforeReady), replay_as_verdict (ReplayIsNotVerdict), ready_on_root_mismatch (ReadyOnlyOnRootMatch), verify_writes_durable (NoEffectBeforeFinalize), nondeterministic_exec (ExecDeterministic), and reconstruct_returns_none, where reconstructing a finalized winner returns None (FinalizedWinnerReconstructs).

Abstracted contracts. MC-04 continues the MC-02 contract ledger, read at v2026.9.0; a pin bump reopens every row. MC-02's K1, K2 (member and set durability), K3 (marshal-path reconciliation) and K9 (ordered at-least-once delivery from marshal) are used by reference.

Id Contract Source at v2026.9.0
K13 Deferred casts a notarize vote once the block is available and its embedded context matches, without waiting for verification; the finalize vote waits on certify, which awaits the verification result consensus/src/marshal/standard/deferred.rs:15-22, :807-825, :318-327, :435-449
K14 Before caching a verified batch the wrapper checks only the sync target, which for qmdb::current is the ops root and operation range; an application using current must itself reject a canonical root mismatch glue/src/stateful/actor/processor/verifier.rs:363-372; glue/src/stateful/db/current.rs:545-549; glue/src/stateful/mod.rs:267-270
K15 The wrapper commits an apply replay during finalization without re-checking block-specific commitments, and a finalized winner that does not execute or does not match its sync targets panics glue/src/stateful/mod.rs:297-304; glue/src/stateful/actor/processor/mod.rs:911-931
K16 Replayed state is reused as parent state and is never a verdict; apply returns None for a block that cannot execute, and the wrapper rejects the ancestry that depends on it glue/src/stateful/mod.rs:74-88, :306-310
K17 Pending state lives only in memory and is lost at restart; verification may be cancelled and retried, and reads through its batches may fall through to the applied database glue/src/stateful/mod.rs:74-80, :272-283
K18 Finalization runs capture with the winning batches, applies them, may start a barrier, then runs finalized with the captured value and readers but no batch; capture is not called for genesis, reconciled, or state-synced blocks glue/src/stateful/actor/processor/mod.rs:939-962; glue/src/stateful/mod.rs:326-337
K19 Simplex agreement: no two conflicting blocks are finalized, so the model keeps one global finalized chain. Trusted, not modelled: the Simplex paper's safety theorem, proved in Lean by NyxFoundation's simplex-fv (section 1); R-18.34 treats consensus as trusted Simplex paper; simplex-fv

Simplex beyond quorum counting, cryptography and the network are not modelled; execution is Exec(parent, block).

Trace binding (VP-07). Traces come from an event log kept only in tests/trace-sim (TE-19), never in a production crate. Its sources: RecordSink::outcome (mode, digest, verdict), the Simplex reporter's activity, the TE-22 per-height roots, the plan actions Crash, Restart and SetStorageFault, and readiness transitions. Crash::Random and Crash::ProcessedHeight crashes appear only as info events on the simulator tracing target (glue/src/simulate/team.rs:148), so the event log subscribes to that target. Each trace fixes a bijection from block digests to model block identifiers. A trace specification in the style of Cirstea, Kuppe, Loillier, and Merz, with hidden steps for the model actions the log does not observe, checks every run of the nightly seed sweep; a failing seed becomes a permanent regression, and every model witness becomes a simulation scenario. The fast configuration's target is under about five million distinct states, reached through symmetry over the honest validators and by restricting block kinds per configuration (the crash-only configuration uses only good and future blocks); deeper bounds run by hand. MC-02's implementation linkage uses the same event log: VP-07 crash runs are checked as traces against MC02RecoveryNode.

8. MC-02 export installation extension (planned)

Status: planned under D50, not written. The export submodel starts from a genesis installation and excludes the exporter's state-sync installation, its (W, A] coverage rule, the standby (R-17.21 beyond its genesis-queue clause, R-17.22) and the retained-window stop (R-17.17) (formal/tla/mc02/README.md, "Abstractions and exclusions"). The extension adds them to MC02RecoveryExport.

Variables. Active and standby queues, each with its queue coverage; the store and mirror watermarks; the validators' retained floor; and an installation target that moves while the sync runs.

Property Requirement
NoLossUnderInstall at each evaluation (every retarget) and at completion of an installation, every height in (W, current target] is published or covered by the other roster member's queue (R-17.21)
StandbyReleasesOnlyBelowObservedWatermark the standby releases an entry only after it observed both the store and the mirror watermark past it (R-17.22)
NoSecondInstall once A is recorded, the node never state-syncs again (R-17.21)
StopWhenUncovered a node whose max(own queue coverage, publication watermark) lies below the retained floor stops and alerts (R-17.21, R-17.17)

Mutations: coverage_at_start_only (coverage evaluated only when the installation starts, caught by NoLossUnderInstall because the target moves), release_on_active_claim (the standby releases on the active exporter's claim rather than an observed watermark, caught by StandbyReleasesOnlyBelowObservedWatermark), and install_below_window (installation proceeds with the watermark below the retained window, caught by StopWhenUncovered). The checker (R-17.19) and the replay job (R-17.20) stay excluded.

9. Non-goals

Recorded under D50, so that no later task spends effort on them without a new decision:

  1. No model of Simplex, marshal, glue, or QMDB internals. They enter MC-02 and MC-04 only through the cited contracts K1 to K19, and "Simplex as configured" stays unscheduled (section 1).
  2. No separate multi-database commit or recovery model; MC-02 covers the member and set barrier contracts.
  3. No DKG or epoch wiring model until DynamicReshareV1 is enabled; the fixed profile has one epoch.
  4. No TLA+ for admission, candidate leases, the exoware query tier, or proof serving; their evidence is the IP-06D and IP-06E acceptance tests, Q5, and the API rows of validation section 6.
  5. No Kani or Aeneas on the asynchronous Stateful adapter; code-level proofs stay on pure functions (section 2, Layer 4).
  6. MC-04 stays small: no crash-cut granularity and no execution values.