vers3: Explicit-State Model Checking Framework

Explicit-state model checking framework for distributed protocol verification, written in Rust. Designed to find safety and liveness violations in multi-actor, multi-step protocols.

Features

• Exact BFS (Bfs) — visited set keyed by full states (hash picks the bucket, equality confirms), so distinct states are never merged by hash collision; produces complete counterexample traces.
• Hashing BFS (BfsHashing) — stores only state hashes (Holzmann-style); scales to larger spaces. Traces are reconstructed by replay and flagged if the replay could not reproduce the recorded path.
• Symmetry reduction — ArraySet<T, N> has a permutation-invariant hash and equality, so states that differ only in the labelling of equivalent agents are genuinely equal and explored once.
• Model errors — rules signal protocol-impossible situations via error_if() / RuleError::model() and get a traced counterexample, instead of panic! aborting without a trace.
• Liveness — LivelockFreedom property detects transient-state cycles.
• Unknowns — rules can return Unknown to signal unresolvable non-determinism without marking the transition as a deadlock.
• Simulation — TransitionSysSimulation checks that one system refines another.
• Counterexample reports — per-step traces with state diffs (report module).

API documentation available with cargo doc; see the crate-level docs for a quick-start example.

Example

An MSI directory cache-coherence protocol model (15,500 states):

cargo run --release --bin example-msi-directory             # hashing BFS
cargo run --release --bin example-msi-directory -- --exact  # exact BFS

Development

make          # format check + tests + clippy
make release  # optimised build

Originally ported from the C++ VerC3 research prototype.