machine-check

Machine-check is a formal verification tool/library for systems described in the Rust programming language, usable for e.g. machine-code or hardware verification.

Get started

Apache 2.0 / MIT License. crates.io

Read the blog

Describe

Describe arbitrary finite-state systems as Finite-State Machines in Rust.

Verify

Automatically verify whether the systems fulfil properties in Computation Tree Logic (CTL).

Visualise

Explore the abstract state space of the system and determine the causes of bugs.