Expand description

A library for model checking systems, with an emphasis on distributed systems.

Most of the docs are here, but a short book is being written to provide a gentler introduction: “Building Distributed Systems With Stateright.”

Introduction to Model Checking

Model implementations indicate how a system evolves, such as a set of actors executing a distributed protocol on an IP network. Incidentally, that scenario is so common for model checking that Stateright includes an actor::ActorModel, and unlike many model checkers, Stateright is also able to spawn these actors on a real network.

Models of a system are supplemented with always and sometimes properties. An always Property (also known as a safety property or invariant) indicates that a specific problematic outcome is not possible, such as data inconsistency. A sometimes property on the other hand is used to ensure a particular outcome is reachable, such as the ability for a distributed system to process a write request.

A Checker will attempt to discover a counterexample for every always property and an example for every sometimes property, and these examples/counterexamples are indicated by sequences of system steps known as Paths (also known as traces or behaviors). The presence of an always discovery or the absence of a sometimes discovery indicate that the model checker identified a problem with the code under test.


A toy example that solves a sliding puzzle follows. This simple example leverages only a sometimes property, but in most cases for a real system you would have an always property at a minimum. The imagined use case is one in which we must ensure that a particular configuration of the puzzle has a solution.

TIP: see the actor module documentation for an actor system example. More sophisticated examples are available in the examples/ directory of the repository

use stateright::*;

#[derive(Clone, Debug, Eq, PartialEq)]
enum Slide { Down, Up, Right, Left }

struct Puzzle([u8; 9]);
impl Model for Puzzle {
    type State = [u8; 9];
    type Action = Slide;

    fn init_states(&self) -> Vec<Self::State> {

    fn actions(&self, _state: &Self::State, actions: &mut Vec<Self::Action>) {
        actions.append(&mut vec![
            Slide::Down, Slide::Up, Slide::Right, Slide::Left

    fn next_state(&self, last_state: &Self::State, action: Self::Action) -> Option<Self::State> {
        let empty = last_state.iter().position(|x| *x == 0).unwrap();
        let empty_y = empty / 3;
        let empty_x = empty % 3;
        let maybe_from = match action {
            Slide::Down  if empty_y > 0 => Some(empty - 3), // above
            Slide::Up    if empty_y < 2 => Some(empty + 3), // below
            Slide::Right if empty_x > 0 => Some(empty - 1), // left
            Slide::Left  if empty_x < 2 => Some(empty + 1), // right
            _ => None
        maybe_from.map(|from| {
            let mut next_state = *last_state;
            next_state[empty] = last_state[from];
            next_state[from] = 0;

    fn properties(&self) -> Vec<Property<Self>> {
        vec![Property::<Self>::sometimes("solved", |_, state| {
            let solved = [0, 1, 2,
                          3, 4, 5,
                          6, 7, 8];
            state == &solved
let checker = Puzzle([1, 4, 2,
                      3, 5, 8,
                      6, 7, 0])
checker.assert_discovery("solved", vec![
        // ... results in:
        //       [1, 4, 2,
        //        3, 5, 0,
        //        6, 7, 8]
        // ... results in:
        //       [1, 4, 2,
        //        3, 0, 5,
        //        6, 7, 8]
        // ... results in:
        //       [1, 0, 2,
        //        3, 4, 5,
        //        6, 7, 8]
        // ... results in:
        //       [0, 1, 2,
        //        3, 4, 5,
        //        6, 7, 8]

The actor and semantics submodules will be of particular interest to most individuals.

Also, as mentioned earlier, you can find more examples in the Stateright repository.


This module provides an Actor trait, which can be model checked using ActorModel. You can also spawn() the actor in which case it will communicate over a UDP socket.

This module provides code to define and verify the correctness of an object or system based on how it responds to a collection of potentially concurrent (i.e. partially ordered) operations.

Utilities such as HashableHashSet and HashableHashMap. Those two in particular are useful because the corresponding HashSet and HashMap do not implement Hash, meaning they cannot be used directly in models.


A Model Checker builder. Instantiable via the Model::checker method.

A path of states including actions. i.e. state --action--> state ... --action--> state.

A CheckerVisitor that records paths visited by the model checker.

A named predicate, such as “an epoch sometimes has no leader” (for which the the model checker would find an example) or “an epoch always has at most one leader” (for which the model checker would find a counterexample) or “a proposal is eventually accepted” (for which the model checker would find a counterexample path leading from the initial state through to a terminal state).

A RewritePlan<R> is derived from a data structure instance and indicates how values of type R (short for “rewritten”) should be rewritten. When that plan is recursively applied via Rewrite, the resulting data structure instance will be behaviorally equivalent to the original data structure under a symmetry equivalence relation, enabling symmetry reduction.

A CheckerVisitor that records states evaluated by the model checker. Does not record generated states that are still pending property evaluation.


Indicates whether a property is always, eventually, or sometimes true.


Implementations perform Model checking.

A visitor to apply to every Path of the checked Model.

This is the primary abstraction for Stateright. Implementations model a nondeterministic system’s evolution. If you are using Stateright’s actor framework, then you do not need to implement this interface and can instead leverage actor::Actor and actor::ActorModel.

This trait is used to reduce the state space when checking a model with CheckerBuilder::symmetry. The trait indicates the ability to generate a representative from a symmetry equivalence class for each state in Model::State.

Implementations can rewrite their instances of the “rewritten” type R based on a specified RewritePlan.