// the find
a16z/halmos
A symbolic testing tool for EVM smart contracts
Halmos is a symbolic execution engine for EVM smart contracts that runs directly against existing Foundry/Solidity test suites — no separate spec language needed. It's aimed at smart contract auditors and security-conscious developers who want to prove invariants hold for all inputs rather than just tested ones.
- Zero-friction adoption for Foundry users: you annotate existing tests with `check_` prefix instead of `test_` and run halmos in place of forge test — no rewrite required.
- Solid regression test coverage across a wide range of EVM features (storage layouts, CREATE2, proxies, TSTORE, signed arithmetic) giving confidence the symbolic executor actually handles edge cases correctly.
- Ships a separate halmos-cheatcodes library that exposes `svm.createUint256`, `svm.createBytes`, etc., giving you typed symbolic variable creation without hacking around test infrastructure.
- Active maintenance with recent commits and a published Docker image bundling solvers (z3, bitwuzla), removing the painful solver-installation step that kills most formal verification tooling adoption.
- Path explosion is a real wall: loops with symbolic bounds, dynamic arrays, and complex DeFi protocols will either time out or require heavy `--loop` and `--width` tuning — the docs don't give enough guidance on where those limits bite in practice.
- The core symbolic EVM interpreter lives in a single `sevm.py` file that is massive; any contributor trying to fix or extend opcode semantics faces a significant orientation cost.
- No native support for multi-transaction / stateful sequences beyond the invariant testing mode, so proving properties that require reasoning about sequences of calls (e.g., reentrancy across separate txs) is awkward or impossible.
- Vyper and Huff support are listed as future plans but absent, so anything not compiled through the Solidity/Foundry pipeline is a non-starter today.