Halmos v0.3.0 release highlights

Halmos v0.3.0 is here!

Halmos is a symbolic testing tool for EVM smart contracts that helps find bugs and verify contract behavior using symbolic execution. Since v0.2.0, we’ve focused on making halmos more effective for practical bug finding, not just formal verification.

This release continues in that direction with support for stateful invariant testing, the most requested feature from our users. To that end, we’ve also added several supporting features, including coverage reports, performance improvements, better solver support, and more.

Stateful invariant testing

Halmos will now look for tests that begin with the invariant_ prefix in addition to stateless check_ tests. When a test contract includes an invariant_ test, halmos will automatically and efficiently:

• discover target contracts (typically contracts deployed during setUp())
• discover target functions (public, state modifying functions of target contracts)
• explore states produced by calling all possible sequences of target functions up to some --invariant-depth (2 by default)
• for each reachable state, assert all invariants and report any failures

Check out a16z/halmos/examples/invariants to get started.

Coverage reports

With --coverage-output lcov.info, halmos outputs coverage information in the standard lcov format. It can be rendered as html with genhtml, or visualized in VSCode using an extension like Coverage Gutters.

Flamegraphs

You can now invoke halmos with --flamegraph. During invariant testing, this will generate call-flamegraph.svg which is a convenient way to visualize all the sequences of calls explored so far.

The generated svgs are interactive, so you can search for FAIL to visualize sequences that lead to a counterexample.

Faster interpreter

We radically optimized the EVM interpreter loop, resulting in up to 32x faster execution.

Better solver support

We have always supported 3rd party SMT solvers with

but this was somewhat hard to use. You needed to bring your own solver (e.g. install or build it yourself). But most importantly you needed to know the right incantations to make it work. For instance, bitwuzla won’t produce counterexamples unless you invoke it with --produce-models and halmos couldn’t parse the counterexamples produced by yices unless you invoked it with --smt2-model-format.

Now you can just give the name of the solver you want to use (e.g. --solver cvc5, --solver yices, --solver z3, …) and halmos will turn it into a full solver command. Halmos will:

• find the solver if you already have it installed (in your PATH or halmos cache)
• offer to install it if you don’t have it and save it in the halmos cache
• invoke it with the right arguments

The lower level --solver-command option is still available for power users, but –solver is the recommended option for most users.

Thanks Josselin for the suggestion! Run halmos --help to see the solvers with a supported configuration.

Yices is the new default solver

Leveraging the improved solver support mentioned previously, we think yices is a better default for most users than z3. It is frequently 3-5x faster, but can occasionally be orders of magnitudes faster.

solx support

In case you missed it: solx is an experimental Solidity compiler based on LLVM. It can be used as a drop-in replacement to solc and works with Foundry, which means it also works with halmos.

To give it a try:

1. Get the latest version of solx from the GitHub releases page.
2. Create a foundry profile:

1. Invoke halmos with the solx profile:

Learn more in the solx release blog post by Matter Labs.

Cheatcode support

We added support for pulling values out of environment variables and .env files with the following cheatcodes:

• envInt(string key)
• envBytes32(string key)
• envAddress(string key)
• envBool(string key)
• envUint(string key)
• envString(string key)
• envBytes(string key)

We also support the array versions (e.g. envAddress(string key, string delimiter) returns (address[]) and the envOr versions with a fallback value (e.g. envAddress(string key, address fallback).

Additionally, we also support the random family of cheatcodes:

• randomAddress()
• randomBool()
• randomBytes()
• randomBytes4()
• randomBytes8()
• randomInt()
• randomInt(uint256 bits)
• randomUint()
• randomUint(uint256 min, uint256 max)
• randomUint(uint256 bits)
• setArbitraryStorage(address target)

These cheatcodes are useful if you want to write tests that work both as foundry fuzz tests and as halmos symbolic tests. Learn more in the foundry book.

Special thanks to Jayakumar for the contributions!

Progress indicators

We now display live progress indicators to get a sense of what halmos is doing during long sessions:

• during path exploration, you will see the number of ops/s (instructions interpreted) as well as the number of completed paths
• during assertion solving, you will see how many queries have been solved and how many queries remain

How to upgrade

By far the easiest way to install and upgrade halmos is to use uv:

1. install uv
2. run uv tool install --python 3.13 halmos
3. run uv tool upgrade halmos