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.

Useful links

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

Just like machine-check, this book is available under the Apache 2.0 or MIT licence. Its original sources are available at GitHub.

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. ↩