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

- URL: https://a16zcrypto.com/posts/article/halmos-v0-3-0-release-highlights
- Authors: [Karmacoma](https://a16zcrypto.com/team/karmacoma), daejun-park
- Published: 2025-07-14
- Updated: 2026-10-02
- Focus areas: code & engineering
- Tags: release notes, Halmos

---

[Halmos v0.3.0](https://github.com/a16z/halmos) 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](https://github.com/a16z/halmos/tree/main/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.

![](https://dwt2zme5yrom6.cloudfront.net/uploads/2025/10/Screenshot-2025-06-19-at-11.23.07-AM.png)

## **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.

![](https://dwt2zme5yrom6.cloudfront.net/uploads/2025/10/image-10-scaled-1.png)

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

![](https://dwt2zme5yrom6.cloudfront.net/uploads/2025/10/image-11.png)

## **Faster interpreter**

We [radically](https://github.com/a16z/halmos/pull/470) [optimized](https://github.com/a16z/halmos/pull/473) the EVM interpreter loop, resulting in up to 32x faster execution.

![](https://dwt2zme5yrom6.cloudfront.net/uploads/2025/10/image-12-scaled-1.png)

## **Better solver support**

We have always supported 3rd party SMT solvers with

```Bash
--solver-command <path/to/solver solver-args>
```

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](https://github.com/montyly) 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](https://github.com/SRI-CSL/yices2) is a better default for most users than z3. It is frequently 3-5x faster, but can occasionally be orders of magnitudes faster.

![](https://dwt2zme5yrom6.cloudfront.net/uploads/2025/10/image-13-scaled-1.png)![](https://dwt2zme5yrom6.cloudfront.net/uploads/2025/10/image-14-scaled-1.png)

## **solx support**

In case you missed it: [solx](https://solx.zksync.io/) 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](https://github.com/matter-labs/solx/releases).
2.  Create a foundry profile:

```Bash
# foundry.toml

[profile.solx]
solc_version = "/usr/local/bin/solx"
```

1.  Invoke halmos with the solx profile:

```Bash
FOUNDRY_PROFILE=solx halmos
```

Learn more in the [solx release blog](https://zksync.mirror.xyz/aCTbO6aDQdrPbUOFR9YMCt24p7-z5KZMMw_GqFz4tpE) 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.](https://getfoundry.sh/reference/cheatcodes/set-arbitrary-storage)

Special thanks to [Jayakumar](https://github.com/Jayakumar2812) 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

![](https://dwt2zme5yrom6.cloudfront.net/uploads/2025/10/halmos-progress-indicator.gif)

## **How to upgrade**

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

1.  [install uv](https://github.com/astral-sh/uv?tab=readme-ov-file#installation)
2.  run `uv tool install --python 3.13 halmos`
3.  run `uv tool upgrade halmos`

---

Source: [Halmos v0.3.0 release highlights](https://a16zcrypto.com/posts/article/halmos-v0-3-0-release-highlights) — a16z crypto. Full archive: https://a16zcrypto.com/posts