The first blogpost on the new website, coinciding with the release of machine-check 0.4.0. Let's talk about what led to this moment.
Have you ever spent days, or even weeks, trying to figure out why your program didn't work the way you expected, only to find that the reason was something completely else, too minor to be even considered, and once you knew what it was, it was fixed in two minutes?
What about something that only happened to the customer a few months after shipping the product, hindering their work until you found out what it was?
I have. And it wasn't very pleasant.
While we have lots of tools today to write software that should be bug-free (such as the Rust language ecosystem), programming embedded systems is still painful and prone to bugs that will leave you in a daze for a few days before you realize you set the wrong bit in the wrong register, which caused memory corruption somewhere down the line. Well, it is still better than writing a program with a bug about which you don't know.
Hi, I'm Jan, the creator of machine-check, a tool for formal verification of digital systems. Elsewhere on this domain, you can learn about its usage with some examples and the underlying research it is based on, so I'll instead recount how machine-check came to be, and the key principles that have arisen throughout.
A little bit of history
Around 2017, during my studies at the Czech Technical University in Prague, I chose to pursue the field of embedded-systems programming. I liked the viscerality, how you can make the system do something you want — even if it is blinking LEDs — and how predicatable the basic operations are when writing in assembly (that gets translated to machine code by the assembler). The reasoning is simple: if you want to know what can happen during an execution of an assembly operation, think about how the data of interest changes as operations are executed, and disregard the rest. If you weren't able to find a good enough answer to your question, think about it in greater detail, focusing on what precluded you from finding out the answer.
While higher-level languages allow you to work much more rapidly, you are now not thinking about what the computer does but what your programming language does when you write something, so it muddles things a bit, and you still have to think about the architecture for good performance and other characteristics. I remember how I converted the reference implementation of Serpent to run on an AVR microcontroller (slowly) for an assignment, making sure the constant S-Boxes were always fetched from the program memory so that the data memory sufficed. Of course, when it gave the wrong result, it took me quite a few hours to find that I missed adding a pgm_read at one place in the code where it was needed. Sometimes you don't win easily.
In 2019, when thinking about what to work on for a diploma thesis, I thought about how I could free myself from the annoying bugs when programming embedded systems by formal verification, which is able to guarantee that the system fulfils a given property. This can be done in theory easily by model checking, building the state space (essentially, a graph) of the system and then verifying the property on it. Unfortunately, the basic idea becomes almost useless in practice as the systems become larger, as the number of states to check tends to rise exponentially (exponential explosion). I was especially inspired by the [mc]square / Arcade.µC model checker from RWTH Aachen, which used the abstraction approach to model-checking: do not consider unimportant data (especially inputs) when building the state space. Unfortunately, the [mc]square project was already defunct, but I made a C++ model checker for simple deadlines inspired by my intuition and their results. Unsurprisingly, while it was able to verify some toy programs, it performed poorly on more complex programs.
Better techniques were needed, and so was the intuition, so I started working on that during my doctoral research. The two main fundamental problems I have encountered were the inability to easily write descriptions of the underlying processors for the machine-code programs, and the low generality of some approaches I tried. A new tool was needed, and I was pleasantly surprised with the speed of development in Rust compared to C++.
On 18th September 2023, I created machine-check, with the intention to describe arbitrary digital systems as Finite-State Machines in Rust and verify them using model checking with abstraction refinement, following the original intuitive idea of thinking in greater detail if the initial abstraction is too coarse. I am happy to say that the approach works, and although there is yet much to be done.
At the start of 2025, machine-check has been selected for a grant from the NGI0 fund by the NLnet foundation. I am happy to say that this has allowed me more time to develop it beyond a research tool, now with a website, a user guide, and an initial version of a graphical user interface. Much remains to be done, but I hope that you will enjoy it nonetheless.
Key principles
- Ease of use. If possible, machine-check should be able to verify completely automatically without requiring the user to reason about it, and the systems and properties shouldn't feel alien.
- Intuitiveness. I feel that for both understandability and scalability, machine-check should think like a reasonable person when performing abstraction and refinement. If something goes wrong (reasonable verification time exceeded or an unexpected verification result), the tool user should be able to understand why that is.
- Soundness. The tool must not return a wrong result. While some verification tools allow a small amount of unsoundness as long as it makes the tool more powerful, I feel that this makes hard to reason about things. While unsoundness can occur due to a bug in machine-check, it is never a feature.
- Generality. While it is usually a lot of work to make sure a general solution – like the use of Rust for program descriptions – to work well, the rewards are worth it, and it can contribute to intuitive understanding that is not limited by the special case.
- Verification power. The tool has to be actually useful to someone, so it should be able to verify something.
The next steps
With the exception of soundness (hopefully), everything can be improved. While I am happy with the current machine-check 0.4.0 as a baseline where the groundwork has been laid, it is now necessary to work on the smaller details: implement more powerful abstractions for better verification power, make the GUI more usable and descriptions more reasonable, implement the checking of more powerful properties.
While we cannot expect miracles from the increase of verification power during one year, the overall user experience should be more streamlined, approachable, and fun at the end of 2025. I will keep you updated throughout on this blog every one or two months.
In the meantime, why not try some verification? Until next time!