Halmos

Open Source

Symbolic bounded model checker for EVM smart contracts. Write tests in Solidity and prove them symbolically using Foundry conventions.

About

Halmos is a symbolic testing tool for EVM smart contracts developed by a]16z. It lets developers write Solidity tests using familiar Foundry conventions that are then verified symbolically rather than with concrete inputs. Halmos bridges the gap between fuzzing and full formal verification, providing stronger guarantees than fuzz testing with less effort than writing formal specifications.