Sign in

README.md

In formal/ · At 62577fb

62577fbHistory

Preview

Text · 3 KiB

mkit formal models

Formal checks of mkit's specifications (formal verification effort). Start with docs/FORMAL.md: it explains the tool split, what each result means (proved, exhaustive, bounded, simulated, tested), the spec-to-property traceability table, the assumptions and the findings. This directory holds the models; each subdirectory's README has the full list of properties, mutants, bounds and recorded results.

DirectoryToolCoversModel
quint/refs/Quint, TLC, ApalacheRef CAS per lock domain, lock order, recovery log, serve.lock and server.lock, served names; refs_mbt.qnt feeds the conformance testref concurrency model, ref conformance model
quint/history/Quint, TLC, ApalacheHistory publication, crash recovery, the scrub scheduleMKIT-20
quint/gc/Quint, TLC, Apalachemkit gc, the recovery log, concurrent writers and the grace window, the server ContentIndex GC orderinggarbage-collection model
quint/transport/Quint, TLC, ApalacheRequested transport identities, shard quorum, release threshold signingtransport model
quint/advance/Quint, TLC, Apalacheadvance_refs, the retry ladder, read_ref disambiguation, the re-baseline gateremote-advance model
lean/Lean 4Merkle inclusion proofs and the delta codec: proofs plus differential tests against RustMerkle proof model, delta model
kani/KaniBounded checks of the untrusted-input decoders (harnesses live next to the Rust code)MKIT-23
scripts/quint, jqgen-refs-traces.sh: regenerates the ITF fixtures for rust/crates/mkit-formal-conformanceref conformance model

Running

From the repository root:

just formal               # quint default mode + lean + conformance
just formal-quint         # every quint/*/check.sh, default mode
just formal-apalache      # the bounded Apalache runs
just formal-lean          # lake build + both difftests
just formal-kani          # every Kani harness, one at a time
just formal-conformance   # replay the refs traces against the code

Each quint/*/check.sh also runs on its own (./check.sh, see its header for knobs). Tool pins and install steps are in docs/FORMAL.md; the nightly workflow is .github/workflows/formal.yml.

Conventions for a new model

  • Cite the spec section each invariant comes from.
  • Give every invariant a mutant or canary that the checker must report as violated, and list the expected outcome of each check in the model's check.sh, which exits 1 on anything unexpected.
  • Record bounds, commands and outcomes in the model's README. Never call a bounded result proved.
  • just formal-quint picks up any new quint/<name>/check.sh automatically.

Files