Halmos

Skill is based on Halmos (a16z/halmos), generated from source at the listed date.

Halmos is a symbolic testing tool for EVM smart contracts. It uses a Solidity/Foundry frontend: you write check_ or invariant_ tests like fuzz tests, and Halmos verifies them for all possible inputs (within bounds) via symbolic execution and an SMT solver. It supports symbolic constructor args, invariant testing over call sequences, and configurable solvers (Yices, cvc5, Bitwuzla).

Core References

Features

Best practices

Generation Info

• Source: sources/halmos
• Git SHA: 079bb4241d1b460baf986257d56ea86977d73451
• Generated: 2026-02-24

Doc paths used

• sources/halmos/README.md
• sources/halmos/docs/getting-started.md
• sources/halmos/examples/README.md
• sources/halmos/examples/simple/README.md
• sources/halmos/examples/invariants/README.md
• sources/halmos/packages/halmos/README.md (Docker only)
• sources/halmos/src/halmos/config.py (CLI and config options)
• sources/halmos/src/halmos/solvers.py (solver names and behavior)
• sources/halmos/src/halmos/build.py (@custom:halmos parsing)
• sources/halmos/src/halmos/__main__.py (invariant depth, frontier)

Best practices for writing symbolic tests

Input conditions: assume vs bound

• Use `vm.assume(condition)` to restrict valid inputs. Inputs that fail the condition are discarded.
• Avoid `bound(x, lo, hi)` in symbolic tests; it tends to perform poorly. Prefer:

  vm.assume(lo <= x && x <= hi);

• Be careful not to over-constrain: too strong assumptions can exclude valid bugs.

Assertions and what Halmos reports

• Halmos reports assertion failures only: reverts with Panic(1) (Solidity assert). Other reverts (e.g. Panic(0), custom errors, arithmetic overflow) are not reported as counterexamples.
• To treat other panic codes as failures: --panic-error-codes 0x01,0x11 or * for all.
• For compilers before 0.8.0 that use INVALID for assert, Halmos does not report those. Use a custom assertion that reverts with Panic(1) (see getting-started.md in the repo).

Checking revert conditions

• If you want to assert that a call reverts under certain conditions, use a low-level call and check the return value:

  (bool success,) = address(token).call(
      abi.encodeWithSelector(token.transfer.selector, receiver, amount)
  );
  if (!success) {
      // assert conditions that imply failure
  }

• This keeps execution going and lets you add assertions about when and why the call fails.

Dynamic arrays, bytes, and string

• Symbolic parameters cannot be dynamic-sized (e.g. bytes, string, uint256[]). Create them inside the test:
• bytes memory data = svm.createBytes(96, 'data');
• Fixed-length array with symbolic elements: uint256[] memory arr = new uint256[3]; then fill with svm.createUint256('elem').
• Control lengths via --array-lengths name1={1,2},name2=3, --default-array-lengths, and --default-bytes-lengths.

Storage layout

• --storage-layout solidity|generic: Use solidity (default) for normal Solidity; use generic for Vyper, Huff, or unconventional Yul storage.

Key points

• Prefer vm.assume over bound; use low-level calls when you need to reason about revert behavior.
• Rely on assert (Panic(1)) for failures Halmos will report; use --panic-error-codes if you need other panic codes.
• Build dynamic types inside the test with svm and optional CLI length options.

<!-- Source references:

• https://github.com/a16z/halmos
• sources/halmos/docs/getting-started.md
• sources/halmos/src/halmos/config.py

-->

setUp and symbolic cheatcodes

setUp and symbolic constructor args

setUp() runs before each test. You can deploy contracts with symbolic constructor arguments so that the test is verified for all possible initial configurations.

Install the Halmos cheatcodes package (separate repo):

forge install a16z/halmos-cheatcodes

Example: ERC20 with symbolic initial supply

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

contract MyTokenTest is SymTest, Test {
    MyToken token;

    function setUp() public {
        uint256 initialSupply = svm.createUint256("initialSupply");
        token = new MyToken(initialSupply);
    }
}

Here svm.createUint256("initialSupply") creates a symbol representing any value in [0, 2^256-1], not a single random value. Halmos then checks the test for every possible initialSupply.

Creating symbols (Halmos cheatcodes)

Symbols can be created in setUp() or inside test functions via the svm (symbolic VM) interface from halmos-cheatcodes. Full list: SVM.sol.

Common patterns:

• Scalars: svm.createUint256("name"), svm.createAddress("name") — name is a label for counterexample output.
• Bytes: svm.createBytes(length, "name") — fixed-length bytes (e.g. 96 for ECDSA).
• Dynamic arrays: Create a fixed-length array and fill elements with symbols:

  uint256[] memory arr = new uint256[3];
  for (uint i = 0; i < 3; i++) {
      arr[i] = svm.createUint256("element");
  }

Dynamic-sized parameters (e.g. bytes, string, uint256[]) cannot be symbolic function parameters; they must be built inside the test with these cheatcodes and optional --array-lengths / --default-*-lengths for length choices.

Foundry vm cheatcodes

Standard Foundry cheatcodes work in Halmos tests: vm.assume, vm.prank, vm.deal, vm.expectRevert, etc. Use vm.assume to constrain symbolic inputs; avoid bound() in symbolic tests in favor of vm.assume(lo <= x && x <= hi).

Key points

• Use SymTest from halmos-cheatcodes/SymTest.sol to get svm.
• Symbolic constructor args make the test cover all possible initial states.
• For bytes/string/dynamic arrays use svm.createBytes, fixed-length arrays filled with svm.createUint256 (or similar), and --array-lengths / --default-bytes-lengths / --default-array-lengths as needed.

<!-- Source references:

• https://github.com/a16z/halmos-cheatcodes
• sources/halmos/docs/getting-started.md
• sources/halmos/README.md

-->

Symbolic testing

Halmos is a symbolic testing tool for EVM smart contracts. It verifies properties for all possible inputs (within bounds) by symbolic execution, rather than sampling random inputs like a fuzzer.

Test naming and structure

• Symbolic tests: functions whose names match the configured prefix (default check_ or invariant_).
• Typical pattern: function check_<function-name>_<behavior>(<symbolic params>) { ... }.
• Same test file can be run with forge test (fuzz) and halmos (symbolic); symbolic runs explore the full input space for the test.

Example:

function check_transfer(address sender, address receiver, uint256 amount) public {
    vm.assume(receiver != address(0));
    vm.assume(token.balanceOf(sender) >= amount);
    uint256 balanceSender = token.balanceOf(sender);
    uint256 balanceReceiver = token.balanceOf(receiver);
    vm.prank(sender);
    token.transfer(receiver, amount);
    assert(token.balanceOf(sender) == balanceSender - amount);
    assert(token.balanceOf(receiver) == balanceReceiver + amount);
}

Symbolic vs random inputs

• In symbolic tests, each parameter is a symbol representing all values of that type (e.g. all uint256 or all address).
• Halmos uses an SMT solver to find any assignment to those symbols that violates an assert.
• Only assertion violations (Panic(1)) are reported as failures; other reverts (e.g. overflow) are not reported unless you use low-level calls or unchecked blocks.

Key points

• Use vm.assume(condition) to restrict valid inputs; inputs not satisfying assumptions are ignored.
• Prefer vm.assume() over bound(); assume is more efficient and clearer in symbolic mode.
• For dynamic arrays / bytes / string, use fixed sizes and create symbols via Halmos cheatcodes (e.g. svm.createBytes(len, 'name')); they cannot be declared as symbolic parameters.
• Counterexamples are printed with concrete values that violate the assertion.

<!-- Source references:

• https://github.com/a16z/halmos
• sources/halmos/README.md
• sources/halmos/docs/getting-started.md

-->