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 result¹, 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.

Useful links

• The main website
• The blog
• Latest stable version at crates.io
• Latest stable API documentation at docs.rs
• Development repository at GitHub