Halmos

Halmos is a symbolic testing tool for EVM smart contracts. It executes Foundry tests symbolically — instead of running with concrete random values like a fuzzer, it reasons about ALL possible inputs simultaneously. When an assertion fails, Halmos produces a concrete counter-example. Built by a16z, it requires no new language (unlike Certora's CVL) and no API key.

GitHub: https://github.com/a16z/halmos Docs: https://github.com/a16z/halmos/wiki

What You Probably Got Wrong

LLMs conflate symbolic testing with fuzzing and full formal verification. These distinctions matter.

Halmos is BOUNDED, not full formal verification — It checks properties up to N loop iterations and call depth. If your contract has an unbounded loop, Halmos verifies correctness only for the iterations you specify via --loop. This is weaker than Certora's unbounded reasoning but catches most real bugs.
Tests look like Foundry tests but execute symbolically — A function check_transfer(address to, uint256 amount) test in Halmos does NOT run with random to and amount. The parameters are symbolic variables representing ALL possible values. Every assert must hold for every combination.
Pre-1.0 software — expect breaking changes — Halmos is under active development. CLI flags, cheatcode support, and output format change between releases. Pin your version in CI.
No API key needed — Unlike Certora Prover (which requires a paid API key and sends code to their cloud), Halmos runs entirely locally using an SMT solver (z3).
vm.assume is NOT require — vm.assume(condition) tells the solver to only consider inputs where condition is true. It prunes the search space. If you over-constrain with too many assumes, you may verify a property only for a trivially small input set.
Symbolic != random — Foundry's fuzzer (forge test) generates random inputs. Halmos's symbolic execution covers EVERY input within bounds. A fuzzer might miss the one value that breaks your invariant; Halmos will find it (if within bounds).
Counter-examples are concrete — When Halmos finds a violation, it outputs specific values (e.g., to = 0x0000...0000, amount = 115792...). These are reproducible as standard Foundry tests.
Not all cheatcodes are supported — Halmos supports a subset of Foundry cheatcodes. vm.assume, vm.prank, vm.deal, vm.store, vm.load work. Complex cheatcodes like vm.ffi and vm.createSelectFork are not supported.