Verification strategy
mxd treats verification as a deliverable, not an afterthought. Each roadmap item includes an explicit verification acceptance criterion alongside its implementation criteria. The tooling spans three layers, chosen to match the risk profile of the property being checked.
Verification boundary
Verification assumes the domain core is a deterministic transition
system:
step(state, event) -> (state', effects).
Wireframe framing, persistence, and object storage live on the
adapter side. That keeps proofs focused on protocol semantics
rather than on incidental I/O mechanics.
Domain side
Server-wide and per-session state, semantic inputs, and semantic effects. This is where handshake gating, privilege rules, drop-box hiding, and news-thread linkage belong.
Adapter side
Wireframe framing, transport timeouts, persistence wiring, and object-store interactions are validated with focused integration tests and harnesses, not treated as the domain's semantic source of truth.
Tool-choice rule: use TLA+ for state-machine progression and policy invariants, Stateright for concurrent interleavings and ordering, and Kani for bounded pure-function invariants and panic freedom.
Specific domain invariants called out in the reference set:
- ▶ Privilege gating: no privileged effect before authentication
- ▶ News threading: linked-list pointer consistency after insert and delete
- ▶ Drop-box visibility: upload-only folders never expose contents to unprivileged sessions
TLA+/TLC
State-machine progression and policy invariants
For state-machine progression and policy invariants. The handshake specification models Idle → AwaitingHandshake → Validating → Ready/Error transitions across multiple concurrent clients with discrete time ticks. TLC explores approximately 10⁶ states at MaxClients = 3 and TimeoutTicks = 5.
INVARIANT NoClientStuckInValidating == \A c \in Clients: (clientState[c] = "Validating") => (\E t \in Nat: t <= TimeoutTicks)
Model checking: TLC verifies that no client remains in the Validating state beyond the timeout threshold, that all successful handshakes reach Ready, and that protocol violations transition to Error without hanging. The same tool class also carries policy invariants such as permissions, drop-box visibility, and news-thread sequencing.
Stateright
Concurrency interleavings
For concurrency interleavings. The session gating model explores login, logout, privilege checks, and out-of-order delivery across multiple clients. It asserts that privileged effects never occur before authentication and that insufficient privileges produce rejections — not silent drops.
fn check_privilege_invariant(state: &SessionState) { for session in &state.sessions { if session.privileged_action_attempted { // Must be authenticated first assert!(session.authenticated); } } }
Interleaving exploration: Stateright systematically explores all possible orderings of concurrent operations. If any sequence allows a privilege escalation or silent failure, the model checker produces a minimal counterexample trace.
Kani
Bounded invariants in pure Rust functions
For bounded invariants in pure Rust functions. Current harnesses prove XOR encode/decode round-trips, header validation predicates, fragment sizing coverage, and transaction ID echoing. This is also the intended home for news-thread pointer updates, permission mapping, and other sharp local invariants that should never panic.
#[kani::proof] fn xor_roundtrip() { let data: [u8; 32] = kani::any(); let encoded = xor_encode(&data); let decoded = xor_decode(&encoded); assert_eq!(data, decoded); }
Proves round-trip correctness for all 32-byte inputs
Validates field bounds and flag combinations
Proves no overflow in fragment reassembly
Reply ID matches request ID in all cases
Regression test integration
Any counterexample trace produced by these tools becomes a regression test that replays the failing sequence through the domain's step function. The verifier finds the bug. The regression test prevents it from coming back.
Counterexample to regression test workflow
Model checker finds violation
TLA+, Stateright, or Kani produces a minimal counterexample trace
Convert to Rust test
Replay the exact sequence of operations through the domain code
Fix implementation
Modify domain logic until the test passes
CI enforcement
Test runs on every commit, preventing reintroduction
Test suite location: Regression tests from verification tools live in tests/regression/ with a comment header citing the original model checker output. This maintains traceability from formal proof to implementation.
Local commands and CI depth
The verification strategy is meant to be runnable, not just admired. Pull requests run a fast subset; nightly jobs deepen the bounds and publish counterexample artefacts for triage.
# TLC via Makefile make tlc-handshake # Stateright models cargo test -p mxd-verification -- --nocapture cargo test -p mxd-verification --test session_gating -- --nocapture # Kani harnesses cargo kani -p mxd --harness kani_validate_header_matches_predicate cargo kani -p mxd --harness kani_reply_header_echoes_id cargo kani -p mxd --harness kani_xor_bytes_round_trip_bounded cargo kani -p mxd --harness kani_login_extras_boundary_gate
Pull requests
Run the critical TLC specs, conservative Stateright bounds, and the highest-value Kani harnesses so verification stays fast enough to gate review.
Nightly jobs
Increase the exploration bounds, run the deeper verification set, and publish any counterexample artefacts so failures can be triaged without guessing what the model checker found.
Three layers, one goal
The verification strategy uses three complementary tools because different properties require different proof techniques. TLA+ models abstract state machines. Stateright explores concrete Rust implementations. Kani proves mathematical properties about pure functions. Together they provide defence in depth.
State machines
Protocol flow correctness
Concurrency
Race condition elimination
Function proofs
Mathematical guarantees