stateright

Stateright is a Rust library that embeds a model checker directly in your code, so you can exhaustively (or randomly) explore the state space of a distributed algorithm and catch nondeterminism bugs — message reordering, dropped packets, duplicate delivery — before they show up in production. You describe a system by implementing the Model trait, then hand it to a CheckerBuilder that runs parallel BFS, DFS, or simulation search strategies across threads.

Beyond pure model checking, Stateright ships an ActorModel and a real actor runtime, so the same actor implementation can be checked inside the model checker and then spawned on an actual UDP network without being rewritten. It also includes linearizability and sequential-consistency testers that can run inside the checker for more exhaustive coverage than black-box tools like Jepsen, plus a built-in Explorer web UI for interactively browsing discovered states and counterexamples in a browser.

What You Get

• A Model trait and CheckerBuilder for describing arbitrary state-transition systems and exhaustively or randomly exploring their state space across parallel threads.
• An ActorModel and real actor runtime so the same actor code runs under the checker for verification and on a live UDP network for production use.
• Linearizability and sequential-consistency testers that run inside the checker for more exhaustive coverage than black-box testing tools like Jepsen.
• An embedded Explorer web UI (backed by tiny_http) for interactively browsing discovered states and counterexample paths in a browser while a check runs.
• Runnable examples covering Paxos, two-phase commit, and linearizable/sequential-consistency registers, checkable or spawnable straight from the CLI.

Common Use Cases

• Verifying a consensus protocol implementation (Paxos, Raft) for safety violations before shipping it.
• Testing whether a distributed key-value store’s actor logic stays linearizable under lossy or duplicating network conditions.
• Exploring a distributed algorithm’s reachable state space interactively via the Explorer UI for teaching or debugging.
• Wiring model-checked properties into CI so state-space regressions are caught the same way unit tests catch logic regressions.

Under The Hood

Architecture The core of Stateright is the Model trait plus CheckerBuilder in src/checker.rs, which dispatches to one of several exploration strategies implemented as private submodules — checker/bfs.rs and checker/dfs.rs run parallel breadth-first and depth-first state-space search sharding work across OS threads via a job-broker and deduplicating visited states in a concurrent DashMap, while checker/simulation.rs offers randomized exploration for state spaces too large to exhaust. checker/path.rs and checker/rewrite.rs/rewrite_plan.rs reconstruct discovery paths and support symmetry-reduction rewrites to shrink equivalent states, and checker/explorer.rs exposes the whole search live over an embedded tiny_http server. Layered on top of this core, src/actor.rs and src/actor/ add an optional ActorModel with a real spawn-on-a-network runtime (actor/spawn.rs, actor/network.rs), and src/semantics/ adds consistency testers (linearizability, sequential consistency) that plug into the same checker rather than requiring a separate tool. Changing the core Model/Fingerprint representation would ripple through every search strategy and every higher-level module, but the trait boundaries keep actors and semantics testers genuinely optional additions rather than required scaffolding.

Tech Stack A Rust 2021-edition crate with no async runtime — parallel search uses native std::thread with JoinHandles. Key dependencies: dashmap and parking_lot for concurrent, lock-protected shared state during multi-threaded search; ahash and nohash-hasher for fast fingerprint hashing; crossbeam-utils for synchronization primitives; serde/serde_json for serializing states to the Explorer UI and reports; rand for randomized simulation checking; and tiny_http to serve the embedded Explorer, whose front-end is a small vanilla KnockoutJS app checked into ui/ with no separate JS build step. dev-dependencies (env_logger, pico-args, num_cpus) support the example binaries in examples/, each of which exposes check, explore, and spawn CLI subcommands.

Code Quality Unit tests (#[cfg(test)] modules with #[test] functions) are present in nearly every core file — checker, actor, semantics, and util modules alike — and the public API carries extensive /// doc comments (roughly 900 across the crate), including a compiled, tested doc-example in lib.rs. No unsafe code appears anywhere in src/. CI (.github/workflows/rust.yml) runs cargo build, cargo test, cargo fmt --check, and cargo clippy --all-targets --all-features with RUSTFLAGS=-Dwarnings on every push and PR to master, so both formatting and lint warnings fail the build. unwrap() appears fairly often (~80 call sites), mostly on internal invariants inside the search/threading machinery rather than on user-facing inputs.

API Design The public surface centers on one trait (Model) with four required methods (init_states, actions, next_state, properties), which keeps the entry point small: implement the trait, call .checker(), choose .spawn_bfs()/.spawn_dfs()/.spawn_simulation(), and call .assert_properties(). The builder pattern (CheckerBuilder) surfaces optional knobs — thread count, symmetry reduction, target state count/depth — without cluttering the required path, and a #[must_use] annotation on the builder guards against the easy mistake of building a checker and forgetting to run it. Extending into actor systems or consistency testing is additive (ActorModel, semantics::*) rather than requiring the base Model API to change, which keeps the learning curve incremental.