halmos by hairyf/blockchain-master

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

Topic	Description	Reference
Symbolic testing	How symbolic tests differ from fuzz tests; check_ structure; vm.assume vs bound	core-symbolic-testing
CLI and config	Invocation, --contract/--function, halmos.toml, @custom:halmos annotations	core-cli-config
setUp and cheatcodes	Symbolic constructor args; svm.createUint256, createAddress, createBytes; halmos-cheatcodes	core-setup-cheatcodes

Features

Topic	Description	Reference
Invariant testing	invariant_ prefix, --invariant-depth, frontier states, running invariants	features-invariant-testing
Solver options	--solver (yices, cvc5, bitwuzla), timeouts, --solver-threads, --solver-command	features-solver-options

Best practices

Topic	Description	Reference
Writing tests	assume vs bound, assertion Panic(1), revert checks, dynamic types	best-practices-writing-tests