Editor’s note: Halmos is an open source formal verification tool developed by the team at a16z crypto. We’ll regularly share the latest improvements and updates in our release notes, as we add features and improve the tool. Visit the GitHub repo to try Halmos or contribute to the project.
Halmos v0.1.0 is out, and it’s a big release focused on performance and developer experience.
Significant performance improvements will benefit both simple tests and large test suites with complex tests. This will make it easier to get started, iterate, and write more ambitious tests.
credit: Palina Tolmach [https://hackmd.io/@SaferMaker/EVM-Sym-Test]
Better foundry integration
We removed the middleware that abstracted away the build system and instead invoke
forge directly. This results in fewer recompilations and better support for incremental builds, which is great for simple tests where compilation time can dominate. This is particularly true for projects that need to build with
More efficient handling of binary blobs
Our EVM interpreter used to wrap every value (e.g. passing through the stack or memory) as a Z3 bit vector, which had the advantage of being consistent and convenient to build expressions mixing concrete and symbolic values. However, profiling revealed that we spent a significant amount of time creating many small Z3 objects, particularly during
setUp() and contract creation.
We now try to keep large concrete buffers like contract code as concrete values (e.g.
bytes) as much as possible and build Z3 expressions lazily. As a result,
setUp() time is about 3x faster.
Better Z3 integration
First, we reduced the default solver timeouts during the path exploration phase from 1000ms to 1ms which gives on average much better empirical results.
Then we implemented several optimizations to enhance the efficiency of SMT queries. These include using explicit quantifier instantiations to generate quantifier-free queries, employing an alternative encoding of Z3 const arrays with the SMT-LIB standard array theory, and implementing multi-phase queries for nonlinear arithmetic reasoning.
Finally, we avoid creating unnecessary states. Previously, Halmos eagerly created new symbolic states whenever a conditional branch was encountered. Now a new symbolic state is only created when both branches are feasible according to the path query solver.
Altogether, this improves single thread performance by about 2x.
This is the first release where Halmos processes work streams in parallel:
--test-paralleloption spawns a new process for each test function in a contract (improves multi-test performance)
--solver-paralleloption spawns a new thread for each assertion solver within a single test (improves single-test performance)
Enabling these options results in a 2-4x improvement on large test suites. Note that these options are still considered experimental for now, so they are not enabled by default.
Halmos now supports more EVM instructions (
MULMOD…) and Foundry cheatcodes (
vm.etch()…). In practice, this means that halmos should work out of the box on more contracts and existing test suites.
We also released a dedicated repository for halmos-cheatcodes, which makes it easier to create symbolic variables. For instance:
check_ is the new
The default function prefix for halmos tests has changed — a small but significant change:
- before v0.1.0, halmos ran
- starting with v0.1.0, halmos now runs
Previously, halmos would run existing, unmodified tests (both regular and fuzz tests). However this also made it harder to separate tests meant for foundry and tests meant for halmos.
With the new
check_ prefix, we avoid this confusion by default: halmos integrates with your existing tests without insisting on running everything in your test suite (and foundry by default won’t try to run your symbolic tests either).
Suppose you have a codebase with multiple test contracts:
- you can run the tests in
ContractAwith the default settings
- all tests in
- one test in
In order for Halmos to run the entire test suite, you resort to running
halmos --loop 10 --smt-div which makes the tests in
ContractA 10x slower.
Starting with Halmos v0.1.0, you can use custom NatSpec tags:
So in this example, running
halmos with the default settings:
ContractAwith the default (fast) settings
--loop 10 --smt-div
Halmos is open source so if you want to get involved, join the dev Telegram chat and check out the good first issues — there are still plenty of low hanging fruits, from improving testing to implementing missing opcodes and cheatcodes.