Release notes: Halmos v0.1.0

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.

Performance

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.

Tool	1tx	sU+1tx	2tx	Foo/FooBytes	MiniVat	ERC721A
halmos v0.0.8	5.0s	4.9s	5.0s	5.2s	30.6s	24m15s
halmos v0.1.0	1.2s	1.4s	1.5s	1.7s	1.8s	2m59s

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 --via-ir.

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.

Parallel processing

This is the first release where Halmos processes work streams in parallel:

• the --test-parallel option spawns a new process for each test function in a contract (improves multi-test performance)
• the --solver-parallel option 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.

Usability

Expanded coverage

Halmos now supports more EVM instructions (PUSH0, ADDMOD, MULMOD…) and Foundry cheatcodes (vm.store(), vm.load(), vm.etch()…). In practice, this means that halmos should work out of the box on more contracts and existing test suites.

Halmos cheatcodes

We also released a dedicated repository for halmos-cheatcodes, which makes it easier to create symbolic variables. For instance:

• svm.createAddress("receiver")
• svm.createUint256("amount")

check_ is the new test

The default function prefix for halmos tests has changed — a small but significant change:

• before v0.1.0, halmos ransetUp() and test*() functions
• starting with v0.1.0, halmos now runs setUp() and check_*() functions

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

@custom:halmos tags

Suppose you have a codebase with multiple test contracts:

• you can run the tests in ContractA with the default settings
• all tests in ContractB requires --loop 10
• one test in ContractB requires --smt-div

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:

• tests ContractA with the default (fast) settings
• tests ContractB run with --loop 10
• tests check_loopsAndDiv with --loop 10 --smt-div

Next steps

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.