Putting technology from machine-check into use in SMT solvers.
During the last two months, I have started working on type-checking in machine-check. It turns out that combining the theoretical framework of Hindley-Milner type systems with the practical way it is done in Rust is quite hard! However, I have managed to finally settle on an architecture that seems reasonable and I hope things will progress more smoothly from now on.
The more exciting news I have is that machine-check now has two "sibling" tools, the Satisfiability Modulo Theories (SMT) solver Roole and a proof-checker Roolean. Both are freely available under the MIT or Apache 2.0 licence.
Model checking and Satisfiability Modulo Theories (SMT)
To explain the tools, I will explain a bit about model checking and SMT solving. Both are basically techniques to fully automatically answer some kind of a question about some well-defined construct. This can be e.g. a computer program or a hardware system.
Model checking is concerned with systems that can theoretically work for an infinite amount of time and answering questions about the infinitely long paths the system can take (e.g. is the system always in a permitted state, no matter how much time passes?). Satisfiability Modulo Theories, on the other hand, does not have any concept of time: we provide a mathematical formula that can contain e.g. bitvectors and operations on them (defined by the theory) and ask if there exists some assignment of variables that satisfies it (satisfiability of the formula). As an aside, if we only allow Boolean variables in the formula, this is the Boolean satisfiability problem (SAT). Many SMT solvers are based around an underlying SAT solver to achieve good performance.
In a way, we can think of SMT as a weaker form of model checking: if we construct a system that behaves according to the given formula in the first step, we can obtain the satisfiability result by model-checking, asking if there exists a result where the formula is satisfied after the first step. However, in practice, the situation is usually turned around: there are many industrially used SMT solvers that can solve very difficult formulas, and they even can be used to emulate model checking by representing multiple steps of the model-checked system in the formula and showing that the property holds for at least this number of steps (bounded model checking).
Roole: combining both worlds
With Armin Biere, we've had an idea: since machine-check uses its own approach for model-checking without using any underlying SAT or SMT solvers, we could port this approach to a new SMT solver and combine it with well-known SAT/SMT techniques to hopefully get something interesting. And this is exactly what Roole is, a Rust SMT solver combining evaluation with abstract domains from machine-check with classic SAT/SMT techniques.
Helpfully, SMT has a standard SMT-LIB language for encoding problems and lots of curated benchmarks, so Roole is essentially plug-and-play. We currently support the theory of quantifier-free bitvectors, i.e. the formula cannot use quantifiers other than the implicit quantifier in the question (does there exist a satisfying assignment?) and we support variables that correspond to wrapping-integer types (e.g. u32) with the usual operations.
According to our evaluations, the current version 0.1.1 is not nearly as powerful as the major competitors in the 2025 edition of SMT competition such as Bitwuzla, but we still can improve many things. We have submitted Roole to the 2026 edition of the SMT competition for now.
Roolean: trusted results without bugs
A huge problem in formal verification is whether our tool actually produces correct results, since we usually want to use formal verification exactly in the critical situations where a mistake could be catastrophic. A good idea is to make the solver produce some kind of a proof certificate file that can then be checked by a dedicated proof checker tool, mirroring how mathematical research works: one mathematician thinks up a proof, then others also check if it is correct. Unfortunately, if we write the proof checker similarly to the solver, we can easily produce the same kinds of bugs in both tools! And if we make the proof checker simpler, it may require large proof certificates or use much more time than the actual solving.
We have tackled this by writing our proof checker, Roolean, in the Lean programming language that allows formally proving properties of the written code. Using this, we have proven that the implementation of the three-valued bitvector domain in Roolean produces correct results as compared to computation with normal bitvectors. Using this, a result of solving with Roole can be turned into a trusted result by feeding the generated proof certificate into Roolean for proof-checking.
While it is hard to write the required proofs in Lean (at least for me), the result is worth it: I can develop new features without concerns of whether I introduced a bug somewhere, something that I struggled with when writing the μ-calculus model-checking in machine-check in 2025. Also, as Roole and Roolean implement much of the same logic, proof certificates are usually very compact (Roole just "guiding" Roolean on its way instead of spelling everything out) and proof-checking usually takes less time than solving.
The (hopefully) shiny future
Since we went from model checking in machine-check to SMT solving in Roole, we can also extend Roole to support model checking, and figure out a good way to do it while keeping many ideas that have made SMT solvers faster over the years. Furthermore, we can prove that the model-checking algorithms are correct in Roolean. While this would require a lot of work, it would allow machine-check to use the sibling tools as a backend, providing faster and much more trustworthy model checking while retaining the full power of μ-calculus.
Of course, this is still far away, and I need to work on the performance of Roole first. But things look promising. Until next time!