At Galois, we develop formal verification tools that rely on a variety of automated solvers for answering mathematical queries. The main solvers we use are called Satisfiability Modulo Theories (SMT) solvers. These solvers offer the ability to answer questions such as “find me inputs for which a mathematical property holds.” We have found these tools to be very useful. There are a variety of solvers developed that support different problem domains and are very efficient at solving complex constraint systems. Among other things, we have used them to verify the correctness of many cryptographic algorithms in seconds, even though the number of inputs is incredibly large (2^256 possible inputs or even larger).
Last week, we released a Haskell library called What4 we use internally for interacting with different SMT solvers. What4 takes its name from Why3, an OCaml-based framework for connecting programs to solvers.
What4 is designed primarily for making it easier for developers to build new verification and program analysis tools that use SMT solvers. A more complete feature list is below, but we wanted a library that made it easier for developers to programmatically construct expressions and send those expressions to solvers for verification or model finding. What4 leverages Haskell’s powerful type system to help ensure expressions are well-formed. What4 also includes many internal expression simplification rules to keep expressions in a reduced form so the solver encoding is compact.
What4 is available on Github and Hackage:
The README on Hackage has a short tutorial showing how to use What4.
What4’s features include:
- Strongly-typed symbolic expressions using GADTs.
- Sending problems to solvers and parsing back results (including counterexamples).
- Optimization and constant-folding routines to simplify and efficiently encode problems.
- Interaction with a variety of solvers (Z3, Yices, CVC4, Boolector, STP, and dReal).
- Additional support for non-SMT solvers (e.g., ABC, BLT) through libraries available on Github.
- Support for both single file and incremental solver interactions depending on performance priorities.
- Explicit DAG-based term representation to minimize problem size.
- Comprehensive support for real/integer arithmetic, bitvectors, and extensional arrays; limited support for other theories.
- Representation of floating-point values as reals, IEEE, or uninterpreted, with the same what4 program.
- An active team of engineers who use it every day, and are paid to develop and maintain it.
We invite you to play with What4, model things in it, break it, complain about it, and improve it. All feedback is much appreciated.