Symbolic testing tool from a16z crypto that runs your existing Foundry tests against all possible inputs. Treats `assert*` calls as properties to be proved over symbolic state, and natively understands `invariant_*` style stateful tests.
- 01promoting Foundry fuzz tests to formal proofs
- 02stateful invariant verification
- 03checking arithmetic and access-control properties exhaustively
- 04low-friction symbolic testing without learning a DSL
- 05complementing Foundry `forge test`
- uv tool install halmos
- # or: pipx install halmos
- # Requires Foundry (forge) on PATH
Use Halmos to symbolically execute Foundry tests. Write a Foundry test like `function check_NeverInsolvent(uint256 amount) public { vm.assume(amount < type(uint128).max); vault.deposit(amount); assertGe(vault.totalAssets(), vault.totalSupply()); }` — Halmos picks up any function prefixed `check_`, `prove_`, or `test_` and proves the asserts hold for all symbolic inputs. Run `halmos --contract VaultTest --function check_NeverInsolvent`. For stateful properties write Foundry-style `invariant_*` functions in a contract with `setUp()`; Halmos auto-discovers target contracts and explores call sequences up to `--invariant-depth 2` (raise as needed). Use `--solver-threads` and `--storage-layout solidity` to tune SMT performance.
- ⚑Halmos models `block.*`, calls, and storage symbolically by default — assumption mismatches (e.g. expecting `block.timestamp > 0`) cause spurious counterexamples; constrain with `vm.assume(...)` early.
- ⚑Loops bounded by symbolic values are unrolled to `--loop` (default 2); under-bounding silently hides bugs, over-bounding explodes solver time.
- ⚑External calls to unmodeled contracts return symbolic data — for protocol integrations either deploy the real contract in `setUp()` or mock with concrete returns to avoid false positives.
- ⚑Counterexamples are reported as input traces, not gas-realistic transactions — instrumented gas numbers from Halmos are meaningless for production tuning.
- ⚑`invariant_*` mode requires `setUp()` to deploy targets; targets discovered later via `targetContract()` helpers from forge-std are not always picked up — declare them explicitly.