User Guide to machine-check

Formal verification of digital systems made easier

Preface

This is the user guide for machine-check, a tool/library for formal verification of arbitrary digital systems described in the Rust programming language using finite-state machines.

Unlike testing, which determines if a specification holds for a small set of system executions, formal verification can determine whether it holds for all possible executions. While only tiny systems can be verified by brute force, machine-check uses an intelligent approach to make verification of larger and more capable systems possible.

Unlike some other verifiers, machine-check is designed to be sound, never returning a wrong verification result1, and complete, theoretically always returning a result in finite time and memory. While arbitrary finite-systems can be represented, the current focus is on verification of systems comprised of machine-code programs executed on embedded processors.

Interested? Read the Quickstart.

⚠️ Currently, machine-check is in active development, with the version 0.4.0 described in this guide. While the basic building blocks are in place, some details may still change considerably in the future.

🚧 This user guide is still under construction. It should be finished in a few days.

1

In other words, if the wrong verification result is returned, this is always considered a bug in machine-check. If you encounter a bug, please report it.

Quickstart

🎓️ This chapter of the book is still being developed and may change significantly. Please come back in a few days.

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-gui = "0.4.0"

Now you can start using machine-check in Rust. 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>,
    }

    impl ::machine_check::Input for Input {}

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

    impl ::machine_check::State for State {}

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

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

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

        fn next(&self, state: &State, input: &Input) -> 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

Currently, machine-check can verify Computation Tree Logic properties of the systems. Let's start with a very simple property: is the value zero at the start of the computation?

cargo run -- --property "value == 0"
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.09s
     Running `target\debug\hello-machine-check.exe --property "value == 0"`
[2025-03-31T17:17:20Z INFO  machine_check] Starting verification.
[2025-03-31T17:17:20Z INFO  machine_check::verify] Verifying the inherent property first.
[2025-03-31T17:17:20Z INFO  machine_check::verify] The inherent property holds, proceeding to the given property.
[2025-03-31T17:17:20Z INFO  machine_check::verify] Verifying the given property.
[2025-03-31T17:17:20Z INFO  machine_check] Verification ended.
+------------------------------+
|        Result: HOLDS         |
+------------------------------+
|  Refinements:             0  |
|  Generated states:        6  |
|  Final states:            5  |
|  Generated transitions:   6  |
|  Final transitions:       6  |
+------------------------------+

Let's not focus on what the messages or numbers mean and just look at the verification result. Machine-check has determined that the property value == 0 holds, which matches the definition of the init function. Note that if the system had multiple initial states, the convention is to verify whether the property holds in all of them. But since we only have one initial state where value = 0, we don't have to think about this.

Verifying a single state is admittedly quite boring. The real power of the Computation Tree Logic is that we can reason about things temporally, looking into states in the future. For example, we can use the temporal operator AX[a] which means "for all paths, a will hold in the next state" to say "for all paths, value will be 0 in the current state". In machine-check property syntax, we write this as AX![value == 0]. Note the exclamation mark after AX: this is done as the property syntax emulates Rust syntax and it makes a lot of sense to think of the temporal properties as macros, since they change what the variables inside them represent. That aside, let's try to verify.

$ cargo run -- --property "AX![value == 0]"
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.09s
     Running `target\debug\hello-machine-check.exe --property "AX![value == 0]"`
[2025-03-31T17:34:28Z INFO  machine_check] Starting verification.
[2025-03-31T17:34:28Z INFO  machine_check::verify] Verifying the inherent property first.
[2025-03-31T17:34:28Z INFO  machine_check::verify] The inherent property holds, proceeding to the given property.
[2025-03-31T17:34:28Z INFO  machine_check::verify] Verifying the given property.
[2025-03-31T17:34:28Z INFO  machine_check] Verification ended.
+------------------------------+
|    Result: DOES NOT HOLD     |
+------------------------------+
|  Refinements:             1  |
|  Generated states:        8  |
|  Final states:            5  |
|  Generated transitions:   9  |
|  Final transitions:       7  |
+------------------------------+

Of course this does not hold: we can increment the value, so value will no longer be zero in all of the next states! But what about it being zero in at least one next state? That should hold: if the increment_value input is 0, we will retain zero value. Instead of AX[a], we will use the EX[a] operator: there exists a path where a holds in next state. Let's try to verify.

$ cargo run -- --property "EX![value == 0]"
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.10s
     Running `target\debug\hello-machine-check.exe --property "EX![value == 0]"`
[2025-03-31T17:38:09Z INFO  machine_check] Starting verification.
[2025-03-31T17:38:09Z INFO  machine_check::verify] Verifying the inherent property first.
[2025-03-31T17:38:09Z INFO  machine_check::verify] The inherent property holds, proceeding to the given property.
[2025-03-31T17:38:09Z INFO  machine_check::verify] Verifying the given property.
[2025-03-31T17:38:09Z INFO  machine_check] Verification ended.
+------------------------------+
|        Result: HOLDS         |
+------------------------------+
|  Refinements:             1  |
|  Generated states:        8  |
|  Final states:            5  |
|  Generated transitions:   9  |
|  Final transitions:       7  |
+------------------------------+

Wonderful. But we have just started to discover the possibilities.

🎓️ This chapter of the book is still being developed and may change significantly. Please come back in a few days.

Systems

🎓️ This chapter of the book is still being developed and may change significantly. Please come back in a few days.

Let us return to the Quickstart example:

#[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>,
    }

    impl ::machine_check::Input for Input {}

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

    impl ::machine_check::State for State {}

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

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

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

        fn next(&self, state: &State, input: &Input) -> 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. Let us unpack it bit by bit. Do not worry if you do not understand everything.

To enable formal verification of properties of digital systems using more intelligent means than brute-force computation, machine-check transforms them in a Rust macro which is called by placing an attribute #[machine_check::machine_description] on an inner module, in this case called machine_module. The code that goes through the macro is enriched with verification analogues for fast verification. As the macro only supports a small subset of Rust code, it will produce a --- hopefully useful --- error if it does not understand something. However, you can still write any Rust code you want outside the module.

Since the machine_description macro cannot read the outside of the module, it does not assume anything about it, such as that the identifier Clone refers to the trait::std::clone::Clone which is usually imported in the Rust prelude --- you might have changed Clone to mean something else outside. As such, you need to import it in the module using the absolute path ::std::clone::Clone. As referring to ::std::clone::Clone each time it is used is annoying, we bring it in scope with a use declaration, so we can just write Clone again and machine_description knows it really is ::std::clone::Clone.

Onto the more interesting part, the structure input:

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

This defines how the input of the Finite-State Machine (FSM) looks like. Do not worry about the derive line; this is needed simply to ensure that it is sensible to manipulate using machine-check. We define a structure Input that has exactly one field increment_value of type Bitvector<1>. Bitvector is a type provided by machine-check that has no signedness information and wrapping arithmetic operations. The number in angled brackets determines the bit-width, i.e. increment-value has only a single bit. So, basically, the input of the FSM is just a single bit. The next line is:

#![allow(unused)]
fn main() {
    impl ::machine_check::Input for Input {}
}

This just states that our input structure can be used as an input to machine-check machines. Do not worry about it. The state structure is more interesting:

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

    impl ::machine_check::State for State {}
}

There is just one field value in the state, a four bits wide bit-vector. Wonderful, what's next?

#![allow(unused)]

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

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

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

        fn next(&self, state: &State, input: &Input) -> 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,
            }
        }
    }
}

This is where the fun begins. We define a structure System that has no fields and implement a trait ::machine_check::Machine on it that will determine the actual FSM.

#![allow(unused)]
fn main() {
        type Input = Input;
        type State = State;
}

The type declarations say that the input type of the FSM (left-side Input) is the structure Input we defined previously. Similarly, the FSM state type is the structure State. To describe the FSM, we also need is a function that creates the initial states of the FSM and a function that transforms a state to a next state, and this is exactly what we have.

#![allow(unused)]
fn main() {
    fn init(&self, _input: &Input) -> State {
            State {
                value: Bitvector::<4>::new(0),
            }
        }
}

The init function takes the system structure (which has no fields in our case, so is quite useless in this situation) and an input, creating an initial machine state based on that. Our init function just creates a state where value is a four-bit bit-vector with the value zero.

⚠️ Currently, the initialisation function also takes the input structure as an argument, possibly creating multiple initial states. This may change in the future by splitting the concerns.

The state function is a bit more interesting:

#![allow(unused)]

fn main() {
        fn next(&self, state: &State, input: &Input) -> 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,
            }
        }
}

We create a mutable variable next_value based on the value of the current state, and if the input field increment_value is equal to one, we add 1 to the value. Note that despite the Bitvector not having any signedness, addition is the same for unsigned and signed numbers in wrap-around arithmetic, so we can do this nicely here. We then return the next value.

So, we have defined a machine that contains a four-bit bit-vector value that is incremented in each step if increment_value is one, otherwise, it is left as-is.

Command-line Interface

🚧 This chapter of the book is still under construction. Please come back in a few days.

Graphical User Interface

🚧 This chapter of the book is still under construction. Please come back in a few days.

Properties

🚧 This chapter of the book is still under construction. Please come back in a few days.

machine-check-avr

🚧 This chapter of the book is still under construction. Please come back in a few days.

Underlying Research

🚧 This chapter of the book is still under construction. Please come back in a few days.