# Modern invariant testing with halmos

> The initial focus of halmos, our open source smart contract symbolic testing tool, has been to make SMT solving work for stateless property tests. These are a good starting point, and an easy transition from stateless fuzz tests, but they’re not the gold standard for smart contract testing. Indeed, ...

- URL: https://a16zcrypto.com/posts/article/modern-invariant-testing-with-halmos
- Authors: [Karmacoma](https://a16zcrypto.com/team/karmacoma), daejun-park
- Published: 2025-07-28
- Updated: 2026-10-02
- Focus areas: code & engineering
- Tags: release notes, Halmos

---

The initial focus of halmos, [our open source smart contract symbolic testing tool](https://github.com/a16z/halmos), has been to make SMT solving work for stateless property tests. These are a good starting point, and an easy transition from stateless fuzz tests, but they’re not the gold standard for smart contract testing. Indeed, the most requested feature by far was support for stateful invariant tests.

In this post, we go over the invariant testing emulation trick, how to improve it with new cheatcodes, and finally how to completely get rid of it in halmos v0.3.x.

## Recap: emulating invariant testing in a stateless test

Back in 2024, Antonio wrote about [emulating stateful invariant testing in halmos](https://a16zcrypto.com/posts/article/implementing-stateful-invariant-testing-with-halmos/) using some clever tricks. The core idea was that within a single stateless test, you could chain together multiple calls, retaining state between them. Let’s review Antonio’s technique on the [MiniVat example](https://github.com/a16z/halmos/blob/main/examples/invariants/src/MiniVat.sol):

import "forge-std/Test.sol";
import {SymTest} from "halmos-cheatcodes/SymTest.sol";

import {MiniVat} from "src/MiniVat.sol";

contract MiniVatTest is Test, SymTest {
    MiniVat public minivat;

    function setUp() public {
        minivat \= new MiniVat();
    }

    function check\_minivat\_n\_full\_symbolic(bytes4\[\] memory selectors) public {
        for (uint256 i \= 0; i < selectors.length; ++i) {
            assumeValidSelector(selectors\[i\]);
            assumeSuccessfulCall(address(minivat), calldataFor(selectors\[i\]));
        }

        assertEq(
            minivat.debt(),
            minivat.Art() \* minivat.rate(),
            "The Fundamental Equation of DAI"
        );
    }
 
    function calldataFor(bytes4 selector) internal view returns (bytes memory) {
        if (selector \== minivat.init.selector) {
            return abi.encodeWithSelector(selector);
        } else if (selector \== minivat.move.selector) {
            return
                abi.encodeWithSelector(
                    selector,
                    svm.createAddress("dst"),
                    svm.createInt256("wad")
                );
         } else if (selector \== minivat.frob.selector) {
            return abi.encodeWithSelector(selector, svm.createInt256("dart"));
        } else if (selector \== minivat.fold.selector) {
            return abi.encodeWithSelector(selector, svm.createInt256("delta"));
        } else {
            revert();
        }
    }
}

Let’s look at what happens in detail:

1.  halmos sees the `check_minivat_n_full_symbolic(bytes4[] memory selectors)` function, which it identifies as a stateless test
2.  because there is a test to run in `MiniVatTest`, halmos deploys it and runs setUp(), retaining the resulting state as the *initial test state*
3.  then it’s time to run the `check_minivat_n_full_symbolic`. Because it has `bytes4[] memory selectors` as an argument, halmos will instantiate it as a concrete array of symbolic `bytes4` values
4.  the test then loops over the selectors array to generate a call sequence
5.  the call to `calldataFor` is boilerplate to make sure we generate valid symbolic data for each call in the *call* sequence
6.  the call to `assumeValidSelector` is a way to express what *target functions* we’re interested in
7.  the test then makes the calls to `address(minivat)` (the *target contract*)
8.  `assumeSuccessfulCall` rejects calls that revert, which is a way to prune paths during *state‑space exploration*.
9.  finally we can assert the protocol *invariant*

This process also contains the essential ingredients of invariant testing:

-   an initial test state
-   target contracts
-   target functions
-   call sequence generation
-   state-space exploration
-   invariant assertions

Running this test yields a result in 2.8s (note that in the original post it used to take 12.6s):

halmos \--function check\_minivat\_n\_full\_symbolic
 \[⠒\] Compiling...
No files changed, compilation skipped

Running 1 tests for test/MiniVat.t.sol:MiniVatTest 
Counterexample: 
    halmos\_dart\_int256\_ce68fb9\_01 \= 0x400000000000000000000000000000000000000000
    p\_selectors\[0\]\_bytes4\_1801362\_00 \= 0x380dc3ca00000000000000000000000000000000000000000000000000000000
    p\_selectors\[1\]\_bytes4\_616eaf4\_00 \= 0xe1c7392a00000000000000000000000000000000000000000000000000000000
    p\_selectors\_length\_baece6c\_00 = 0x02

\[FAIL\] check\_minivat\_n\_full\_symbolic(bytes4\[\]) (paths: 70, time: 2.75s, bounds: \[selectors\=\[0, 1, 2\]\])
Symbolic test result: 0 passed; 1 failed; time: 2.77s

This works fine on MiniVat, which is a simplified version of the [full Vat contract](https://github.com/a16z/halmos/blob/main/examples/invariants/src/Vat.sol) with just 4 target functions. MiniVat is intentionally simple; the real challenge is breaking the invariant for the full `Vat` contract. The full Vat contract has 16 target functions, which means that if we want to support it we will have a lot of boilerplate to write, and the performance will take a big hit.

Below, we’ll show how to improve the hand-rolled version of the stateful testing framework, and finally how it can be simplified with the latest release of halmos.

![💻](https://s.w.org/images/core/emoji/17.0.2/72x72/1f4bb.png) if you want to follow along, the full code for the examples is available: [https://github.com/0xkarmacoma/halmos-invariants-sandbox](https://github.com/0xkarmacoma/halmos-invariants-sandbox)

## Supporting the full Vat contract, the hand-rolled approach

### Using svm.createCalldata(address)

Halmos now supports some convenient cheatcodes (see [a16z/halmos-cheatcodes](https://github.com/a16z/halmos-cheatcodes/blob/main/src/SVM.sol)):

// Create arbitrary symbolic calldata for the given contract address, name, or interface name.
// By default, view and pure functions are excluded. 
// An optional boolean flag can be set to include view and pure functions.

function createCalldata(
    address contractAddress
) external pure returns (bytes memory);

function createCalldata(
    string memory contractOrInterfaceName
) external pure returns (bytes memory);

function createCalldata(
    string memory filename, 
    string memory contractOrInterfaceName
) external pure returns (bytes memory);

This means we can completely get rid of the `calldataFor` and `assumeValidSelector` helpers!

The code for the full Vat test now looks like this:

import {Test, console} from "forge-std/Test.sol";
import {SymTest} from "halmos-cheatcodes/SymTest.sol";
import {Vat} from "src/Vat.sol";

contract VatTest is Test, SymTest {
    Vat public vat;
    bytes32 public ilk \= "gems";

    function setUp() public {
        vat \= new Vat();
        vat.init(ilk);
    }

    function check\_vat\_n\_full\_symbolic() public {
        uint256  depth \= vm.envOr("INVARIANT\_DEPTH", uint256(2));
        console.log("generating call sequences with depth", depth);

        for (uint256 i \= 0; i < depth; ++i) {
            assumeSuccessfulCall(
                address(vat), 
                **svm.createCalldata(address(vat)) // using the new cheatcode**
            );
        }

        assertEq(
            vat.debt(),
            vat.vice() + vat.Art(ilk) \* vat.rate(ilk),
            "The Fundamental Equation of DAI"
        );
    }

    function assumeSuccessfulCall(address target, bytes memory data) public {
        (bool success, ) \= target.call(data);
        vm.assume(success);
    }
}

This finds a counterexample in 1-2 min:

INVARIANT\_DEPTH\=2 halmos \--function check\_vat\_n\_full\_symbolic \--early-exit
\[⠒\] Compiling...
No files changed, compilation skipped

Running 1 tests for test/Vat.t.sol:VatTest
\[console.log\] generating call sequences with depth 2
Counterexample: 
    p\_dart\_int256\_45a168c\_124 \= 0x200000000000000000000000000000000000000000
    p\_dink\_int256\_0cd2e65\_123 \= 0x00
    p\_i\_bytes32\_ead0d7f\_119 \= 0x00
    p\_ilk\_bytes32\_718b270\_81 \= 0x00
    p\_rad\_uint256\_54a455e\_46 \= 0x8000000000000000000000000000000000000000000000000000000000000000
    p\_selectors\[0\]\_bytes4\_1eee7ca\_00 \= 0x00
    p\_selectors\[1\]\_bytes4\_018ac94\_00 \= 0x00
    p\_selectors\_length\_14577c1\_00 \= 0x02
    p\_u\_address\_b307c2b\_44 \= 0x00
    p\_u\_address\_b5d362f\_120 \= 0x00
    p\_v\_address\_2f08456\_45 \= 0x00
    p\_v\_address\_3bc206a\_121 \= 0x00
    p\_w\_address\_e6be6d6\_122 \= 0x00

\[FAIL\] check\_vat\_n\_full\_symbolic(bytes4\[\]) (paths:  455, time:  61.55s, bounds: \[selectors\=\[0, 1, 2\]\])
Symbolic test result:  0 passed;  1 failed; time:  61.59s

Let’s take a moment to unpack what `svm.createCalldata(address(vat))` is doing:

-   it maps the address back to a contract name based on its deploy code
-   it looks up the ABI for the contract
-   it generates calldata with appropriate symbolic arguments for all public state-mutating functions as well as empty bytes and bytes for the fallback function

![💡](https://s.w.org/images/core/emoji/17.0.2/72x72/1f4a1.png)add `console.logBytes(data)` in `assumeSuccessfulCall` to inspect the calldata bytes that are automatically generated.![null](https://dwt2zme5yrom6.cloudfront.net/uploads/2025/07/image-17.png)

### Using vm.snapshotState()

In AssumeSuccessfulCall, we do `(bool success, ) = target.call(data);` and then `vm.assume(success)`, which lets us ignore calls that reverted.

Because a revert undoes all changes, rejecting reverted calls let us skip paths that we know don’t affect state. But you can have other calls that don’t revert, and also don’t change state! Ideally we would also want to ignore these. Since v0.2.3 we support snapshot cheatcodes, so we can do something like this:

mapping(uint256 \=> bool) public visited;

function check\_vat\_n\_full\_symbolic() public {
    uint256 depth \= vm.envOr("INVARIANT\_DEPTH", uint256(2));
    console.log("generating call sequences with depth", depth);

    // record the initial state snapshot
    **visited\[vm.snapshotState()\] \= true;**

    for (uint256 i \=  0; i &lt depth; ++i) {
        assumeSuccessfulCall(
            address(vat), 
            svm.createCalldata(address(vat))
        );

        **uint256 snapshot \= vm.snapshotState();**

        // skip if the snapshot has already been visited
        **vm.assume(!visited\[snapshot\]);**
    
        // keep track of new snapshots
        **visited\[snapshot\] \= true;**
    }

    assertEq(
        vat.debt(),
        vat.vice() + vat.Art(ilk) \* vat.rate(ilk),
        "The Fundamental Equation of DAI"
    );
}

In halmos, `snapshotState()` returns a hash of the network state (storage, balance, account code) which means we can compare snapshots. If the network state has not changed at all, then the snapshot should also be unchanged.

Unfortunately this does not result in an actual speedup because of the overhead of touching storage in Solidity, but the idea itself is sound. We just need some help from halmos itself. The last section covers how halmos v0.3 helps.

### Enabling arbitrary timestamp, value and sender

There are a few remaining problems with our current approach that limit its generality:

-   the sender is fixed, every call comes from the test address `(address(this)`)
-   the block timestamp never changes
-   we never send any value, so payable functions in the target contract are not properly explored

We could address these issues by modifying `assumeSuccessfulCall`:

function assumeSuccessfulCall(address target, bytes memory data) public {
    // allow any sender and value for this call
    address sender \= svm.createAddress("sender");
    uint256 value \= svm.createUint256("value");
    vm.deal(sender, value);

    // also allow any block timestamp to simulate calls in different blocks
    uint256 timestamp \= svm.createUint256("timestamp");
    vm.assume(timestamp &gt= block.timestamp);
    vm.warp(timestamp);

    vm.prank(sender);
    (bool success, ) \= target.call{value: value}(data);
    vm.assume(success);
}

With these new modifications, our more general but still hand-rolled stateful testing “framework” can now break the DAI invariant in 3 minutes:

halmos \--function check\_vat\_n\_full\_symbolic \--early-exit
 \[⠒\] Compiling...
 \[⠃\] Compiling 1 files with Solc 0.8.28
 \[⠊\] Solc 0.8.28 finished in 776.31ms
Compiler run successful!

Running 1 tests for test/Vat.t.sol:VatTest
\[console.log\] generating call sequences with depth 2
Counterexample: 
    halmos\_sender\_address\_80cde3f\_47 \= 0x7fa9385be102ac3eac297483dd6233d62b3e1496
    halmos\_sender\_address\_97bc225\_96 \= 0x7fa9385be102ac3eac297483dd6233d62b3e1496
    halmos\_timestamp\_uint256\_afd7084\_49 \= 0x8000000000000000000000000000000000000000000000000000000000000000
    halmos\_timestamp\_uint256\_e79e87f\_98 \= 0x8000000000000000000000000000000000000000000000000000000000000000
    halmos\_value\_uint256\_1dc9b21\_48 \= 0x00
    halmos\_value\_uint256\_6e7e9ac\_97 \= 0x00
    p\_dart\_int256\_749817d\_32 \= 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
    p\_dink\_int256\_a5650cc\_31 \= 0x00
    p\_i\_bytes32\_30b6237\_27 \= 0x00
    p\_i\_bytes32\_8de9b03\_62 \= 0x00
    p\_rate\_\_int256\_9900444\_64 \= 0x01
    p\_u\_address\_482aaa5\_28 \= 0x00
    p\_u\_address\_e8dc543\_63 \= 0x00
    p\_v\_address\_74d52aa\_29 \= 0x00
    p\_w\_address\_c739174\_30 \= 0x00

\[FAIL\] check\_vat\_n\_full\_symbolic() (paths: 1091, time: 179.83s, bounds: \[\])
Symbolic test result: 0 passed; 1 failed; time: 179.89s

Up until the release of halmos v0.3.0, this was likely the best way to emulate stateful invariant testing.

## Putting it all together with modern halmos

Since halmos v0.3.0 supports invariant testing out of the box, we can rewrite the test as follows:

import "forge-std/Test.sol";

import {Vat} from "../src/Vat.sol";

/// @custom:halmos --early-exit --invariant-depth 2
contract VatTest is Test {
    Vat public vat;
    bytes32 ilk;

    function setUp() public {
        vat \= new Vat();
        ilk \= "gems";

        vat.init(ilk);
    }

    function invariant\_dai() public view {
        assertEq(
            vat.debt(),
            vat.vice() + vat.Art(ilk) \* vat.rate(ilk),
            "The Fundamental Equation of DAI"
        );
    }
}

All the helpers and the boilerplate are gone! Also note that there is no need for bounding or clamping. We just explore the state-space with completely unbounded values and let the symbolic engine discover constraints.

Under the hood, halmos implements all the features we previously had to roll out manually:

-   target contract selection (in this case just `Vat`, because it was deployed during `setUp()`
-   target function selection (all public functions of `Vat`)
-   symbolic calldata generation for each target function
-   visited state snapshots
-   arbitrary senders, value and block timestamps
-   command line option to set the max call sequence length (`--invariant-depth`)

---

To give it a try, upgrade to the latest release:

1.  [install uv](https://github.com/astral-sh/uv?tab=readme-ov-file#installation)
2.  run `uv tool install --python 3.13 halmos` if you don’t already have halmos installed
3.  run `uv tool upgrade halmos` if you already have a uv install of halmos

Then check out the [invariant testing examples](https://github.com/a16z/halmos/blob/main/examples/invariants/README.md). To run the final example in this post:

git clone git@github.com:a16z/halmos.git
halmos \--root halmos/examples/invariants \--function invariant\_dai

\*\*\*

*Thanks to [aviggiano](https://github.com/aviggiano) and [igorganich](http://github.com/igorganich) for providing feedback on early versions of this post.*

\*\*\*

*The views expressed here are those of the individual AH Capital Management, L.L.C. (“a16z”) personnel quoted and are not the views of a16z or its affiliates. Certain information contained in here has been obtained from third-party sources, including from portfolio companies of funds managed by a16z. While taken from sources believed to be reliable, a16z has not independently verified such information and makes no representations about the current or enduring accuracy of the information or its appropriateness for a given situation. In addition, this content may include third-party advertisements; a16z has not reviewed such advertisements and does not endorse any advertising content contained therein.*

This content is provided for informational purposes only, and should not be relied upon as legal, business, investment, or tax advice. You should consult your own advisers as to those matters. References to any securities or digital assets are for illustrative purposes only, and do not constitute an investment recommendation or offer to provide investment advisory services. Furthermore, this content is not directed at nor intended for use by any investors or prospective investors, and may not under any circumstances be relied upon when making a decision to invest in any fund managed by a16z. (An offering to invest in an a16z fund will be made only by the private placement memorandum, subscription agreement, and other relevant documentation of any such fund and should be read in their entirety.) Any investments or portfolio companies mentioned, referred to, or described are not representative of all investments in vehicles managed by a16z, and there can be no assurance that the investments will be profitable or that other investments made in the future will have similar characteristics or results. A list of investments made by funds managed by Andreessen Horowitz (excluding investments for which the issuer has not provided permission for a16z to disclose publicly as well as unannounced investments in publicly traded digital assets) is available at https://a16z.com/investments/.

Charts and graphs provided within are for informational purposes solely and should not be relied upon when making any investment decision. Past performance is not indicative of future results. The content speaks only as of the date indicated. Any projections, estimates, forecasts, targets, prospects, and/or opinions expressed in these materials are subject to change without notice and may differ or be contrary to opinions expressed by others. Please see https://a16z.com/disclosures for additional important information.

---

Source: [Modern invariant testing with halmos](https://a16zcrypto.com/posts/article/modern-invariant-testing-with-halmos) — a16z crypto. Full archive: https://a16zcrypto.com/posts