FORMAL.md

Formal verification

mkit checks parts of its specifications with formal tools: model checkers for the concurrent and crash-recovery protocols, a proof assistant for two pure algorithms, a bounded model checker for the untrusted-input decoders, and a replay harness that ties one model back to the code. This page says what each check covers, how strong its result is, what it assumes, and what it found. The per-model READMEs under formal/ hold the full detail: every invariant, mutant, bound, state count and run time.

The formal verification effort integrates the Quint and Lean models and was done against the specs on the feat/mkit-server line (PR #1082). The spec text is normative. Where a model found the spec wrong, the spec was fixed; where it found the code wrong, the code was fixed with a regression test, or the gap is listed under Open findings.

How strong is a result

Every result on this page carries one of these labels. Read them literally.

"Bounded" never means "proved". Only the Lean theorems are proofs, and only for the model: the link from the Lean model to the Rust code is a differential test, not a proof.

Non-vacuity. A property that holds could hold because it is too weak or because the model never reaches the interesting states. Every invariant here is therefore paired with evidence that it can fail:

• a mutant, a copy of the model with one deliberate bug, which the checker must report as a violation of that specific invariant;
• a canary, a false reachability claim ("no gc ever deletes anything") the checker must refute, which shows the states that matter are reached;
• for Lean, a *_needed or mutant_* lemma showing that each hypothesis and each check is load-bearing;
• for Kani, a *_canary_* harness marked #[kani::should_panic].

Each check.sh prints one line per check with its expected outcome (ok or violation) and exits 1 on anything unexpected, so a mutant that stops failing breaks the run just like an invariant that stops holding.

Tool split

Why no standalone TLA+. The protocol models are written once, in Quint, and TLA+ is generated from them. Hand-written TLA+ would be a second copy of each model that could drift from the Quint one that the tests and simulations use. The only hand-written TLA+ is formal/quint/history/tlc/: thin wrappers that add a state VIEW and fairness to the compiled output. TLC runs as a checker, not as a modelling language.

Traceability

One row per property that a spec clause depends on. "Status" is the strongest label the property has; weaker checks (simulation, scenario tests) also run on every row. Bounds are the defaults in each check.sh. The linked READMEs list every property; this table lists the ones a spec reader is most likely to look for.

Refs, locks and servers (formal/quint/refs, ref concurrency model)

Garbage collection (formal/quint/gc, garbage-collection model)

History publication and scrub (formal/quint/history, MKIT-20)

Remote advance (formal/quint/advance, remote-advance model)

Transport identity, shards, threshold (formal/quint/transport, transport model)

Merkle objects and delta (formal/lean, Merkle proof model, delta model)

Decoders (formal/kani, MKIT-23)

Assumptions

Each result holds only under these assumptions. They are stated in the model or harness that relies on them.

• Hashes. Lean theorems take injectivity of the node, leaf, finalize and wrap hashes as explicit hypotheses (NodeInj, LeafInj, FinInj, WrapInj), not as axioms; termHasher (a free term algebra) satisfies all of them, so the theorems are not vacuous. The Quint transport models treat BLAKE3 as the identity on contents (collision resistance) and BLS signatures as symbolic (unforgeability, no interpolation across polynomials). Kani harnesses replace BLAKE3 with a deterministic mixer and stub zstd decompression.
• Bounds. Every Quint result is for the fixed instance in its README: a handful of processes (2 or 3), objects (up to 8), commits (up to 7) and clock values. Apalache lengths are 4 to 16 steps. Kani inputs are a few bytes to 125 bytes. Constants are scaled where the real ones are too large (for example the scrub model uses MIN_WINDOW=2 for 512 and MAX_AGE=3 for seven days, keeping the relation that matters, and a separate test checks the real constants).
• Time and crashes. Time is a small integer clock. Lock waits never time out. A crash is one atomic step that discards volatile state; history recovery liveness assumes finitely many crashes and fair callers.
• Abstractions of the code. Each model follows specific Rust functions, named in its README, and abstracts I/O: a durable write is one step, a lock is a set membership. A mismatch between a model step and the code it names is a modelling error these checks cannot catch; the reviews on ref concurrency model through remote-advance model compared each model with the code by hand, and ref conformance model replays one model against the code.
• Lean to Rust. The Lean models are executable specifications. Their agreement with merkle.rs and delta.rs rests on the differential tests (sampled vectors), not on a proof.

Findings

What the models found, and where each stands. "Fixed" means the code changed, with a regression test that fails before the fix and passes after.

Fixed in code

Fixed in the spec

The models also found spec text that was wrong or incomplete, and the spec was corrected on this branch: the scrub lap is at most 65 publishes, not 64, and that bound needs the scrub write to land (SPEC-HISTORY-PROOF §4.5); SPEC-GC now states the normative writer condition T - mtime < grace; SPEC-TRANSPORT §7 and SPEC-TRANSPORT-CONNECT now agree on the retry and read_ref obligations; SPEC-MERKLE-OBJECTS §5.4 states the builder refusal. The per-model READMEs list each change.

Open findings

None of these has its own Linear issue yet; each is recorded under the issue whose model found it.

Limitations

• Bounded is not proved. Outside Lean, every result covers a finite instance, a bounded length or a bounded input size. Larger instances are argued, not checked; several READMEs record checks that did not finish within the 30-minute budget and were cut back.
• Not everything is checked by every tool. Some invariants are checked only by simulation and Apalache (for example WindowOnlyWhenFresh), some liveness properties only on the smaller instances (Termination on two pushers), and some mutants only by quint run and TLC. The per-model READMEs say which.
• Models follow the code by hand. Only the refs model is replayed against the implementation (ref conformance model), and only for 5 sampled traces. Lock steps, the history-mmr ancestry path and age-based recovery pruning are not compared.
• Not modelled. Among others: pack GC, ledger expiry, MAX_REACHABLE truncation, SQLite-backed server metadata, the S3 spool sweep, the git bridge locks, the shard byte budget, multi-entry trees in Kani, and every decoder input beyond the Kani bounds (left to fuzzing and proptests).
• Tool trust. Results trust Quint's compiler to TLA+, Apalache, TLC, CBMC and the Lean kernel. Tool versions are pinned; the Apalache jar is checked by sha256.

Run the checks

The just recipes run every layer and are what .github/workflows/formal.yml runs nightly (and on workflow_dispatch). Each prints one line per check and fails on any unexpected outcome. Times below are from a shared 15-core arm64 Mac. just formal is the smallest useful set, but at about an hour it runs nightly rather than on every PR; most of it is the quint run simulations of the refs model.

Install the tools

The pins live in the formal_* variables at the end of the justfile, and formal.yml repeats them.

On macOS:

brew install openjdk@21 elan-init just jq node
npm install -g @informalsystems/quint@0.32.0
just formal-setup-apalache      # Apalache 0.62.2 into ~/.local/share/mkit-fv, sha256-checked
cargo install --locked kani-verifier --version 0.68.0 && cargo kani setup

The check.sh scripts find Homebrew's keg-only openjdk@21 on their own. elan reads formal/lean/lean-toolchain and fetches Lean v4.34.0 on the first lake build.

On Linux, install a Java 21 JDK (for example apt install openjdk-21-jdk-headless) and set JAVA_HOME to it, install Node.js, jq and elan, then run the same npm, just formal-setup-apalache and cargo install commands.

FV_HOME (default ~/.local/share/mkit-fv) moves the Apalache install; APALACHE_MC and TLA2TOOLS point at another copy. Each check.sh documents its own knobs (ONLY, SEL, TLC_HEAP, *_DEPTH).

Resource use

TLC runs with a 4 GB heap and 2 to 4 workers, Apalache with 4 GB. The largest Kani harness peaks at about 5.4 GB. Run one Kani harness at a time. The recorded times come from a 15-core arm64 Mac shared with other jobs; a CI runner is slower.