Quickstart

If you are a Rust user, you can skip to the usage. You can also try out the quick example from the machine-check readme.

Setting up Rust

Machine-check is a tool for verification of systems written in a subset of the Rust programming language. In the context of Rust, it works as a library you use in your code. If you do not use Rust yet, you need to install Rust and learn its basics first. Fortunately, describing finite-state machines does not use that many Rust concepts, so you can just skim over the first few chapters (although preferably 10) of the Rust Book, try out a few examples, and return to the book if you do not understand something.

To start using machine-check, create a new binary Rust package using Rust's package manager cargo:

$ cargo new hello-machine-check      
    Creating binary (application) `hello-machine-check` package
note: see more `Cargo.toml` keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

In the created hello-machine-check directory, there is a package config file Cargo.toml and a hello-world placeholder in src/main.rs:

fn main() {
    println!("Hello, world!");
}

You can run the program using cargo run in the hello-machine-check directory:

$ cargo run
   Compiling hello-machine-check v0.1.0 (<your path>\hello-machine-check)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 1.07s
     Running `target\debug\hello-machine-check.exe`
Hello, world!

Let us now move to actually using machine-check.

Using machine-check

In your Cargo.toml, add the following dependency:

[dependencies]
machine-check = "0.6.0"

You can start using machine-check in Rust now. Let's create a minimal somewhat interesting system to verify. Put this in your src/main.rs:

#[machine_check::machine_description]
mod machine_module {
    use ::machine_check::Bitvector;
    use ::std::{
        clone::Clone,
        cmp::{Eq, PartialEq},
        fmt::Debug,
        hash::Hash,
    };

    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
    pub struct Input {
        increment_value: Bitvector<1>,
    }

    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
    pub struct Param {}

    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
    pub struct State {
        value: Bitvector<4>,
    }

    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
    pub struct System {}

    impl ::machine_check::Machine for System {
        type Input = Input;
        type Param = Param;
        type State = State;

        fn init(&self, _input: &Input, _param: &Param) -> State {
            State {
                value: Bitvector::<4>::new(0),
            }
        }

        fn next(&self, state: &State, input: &Input, _param: &Param) -> State {
            let mut next_value = state.value;
            if input.increment_value == Bitvector::<1>::new(1) {
                next_value = next_value + Bitvector::<4>::new(1);
            }

            State { value: next_value }
        }
    }
}

fn main() {
    let system = machine_module::System {};
    machine_check::run(system);
}

That is a lot of code. Fortunately, most of it is just boilerplate around the contents of the Input and State structures and init and next functions which define a Finite State Machine. We will discuss how the machine is described later; for now, just know that the state contains a four-bit field value that is initially zero and after that, each next step of the machine is determined by looking at a single-bit input field increment_value, incrementing value if increment_value is 1 and leaving value as-is otherwise. Ready for some verification?

Verifying

Machine-check can verify properties in propositional μ-calculus. For simplicity, we will discuss verifying Computation Tree Logic (CTL) properties in the main part of the book and discuss the μ-calculus in an advanced chapter. For example, using a CTL property, we can determine that from every reachable state of the system, we can, through some sequence of inputs, get to a state where value is zero:

$ cargo run -- --property 'AG![EF![value == 0]]'
   Compiling hello-machine-check v0.1.0 ((...)\hello-machine-check)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 1.36s
warning: the following packages contain code that will be rejected by a future version of Rust: partitions v0.2.4
note: to see what the problems were, use the option `--future-incompat-report`, or run `cargo report future-incompatibilities --id 1`
     Running `target\debug\hello-machine-check.exe --property "AG![EF![value == 0]]"`
[2025-08-25T17:23:24Z INFO  machine_check] Starting verification.
[2025-08-25T17:23:24Z INFO  machine_check::verify] Verifying the inherent property first.
[2025-08-25T17:23:24Z INFO  machine_check::verify] The inherent property holds, proceeding to the given property.
[2025-08-25T17:23:24Z INFO  machine_check::verify] Verifying the given property.
[2025-08-25T17:23:24Z INFO  machine_check] Verification ended.
+-------------------------------+
|         Result: HOLDS         |
+-------------------------------+
|  Refinements:             16  |
|  Generated states:        48  |
|  Final states:            16  |
|  Generated transitions:   64  |
|  Final transitions:       33  |
+-------------------------------+

Machine-check was able to quickly verify that the supplied property holds.

🛠️ You can safely ignore the warning about the package partitions, which is currently internally used by machine-check. This warning should be rectified in the next release.

While the example system under verification is very simple, machine-check integrates advanced techniques that make verification of more complex systems possible, such as ones combining a processor and a machine-code program. In the following chapters, we will discuss the properties that can be verified, the system descriptions, the Command-line Interface, and the Graphical User Interface that can be used to understand the results of verification or the reasons for the inability to feasibly verify a property against a system.