用途：Halmos 是面向 EVM 智能合约的符号测试工具，用符号执行方式运行 Foundry 测试，而非像模糊测试那样使用随机具体值。它同时推理所有可能输入，断言失败时输出可复现的具体反例。由 a16z 开发，无需新语言（不同于 Certora 的 CVL），也无需 API key。
主要能力：以 check_ 前缀函数作为符号测试，参数自动成为符号变量；支持 assert() 属性检查；支持 vm.assume、vm.prank、vm.deal、vm.store、vm.load 等部分 Foundry cheatcode；通过 halmos-cheatcodes 的 svm 构造器创建符号存储值；支持循环边界（--loop）、调用深度（--depth）、求解器超时等配置；可读取 foundry.toml，也支持 halmos.toml 专用配置。
使用方式：需 Python 3.12+、Foundry 及已编译合约。安装：pip install halmos；验证：halmos --version；CI 中可固定版本如 pip install halmos==0.2.1。编写 check_ 前缀测试后运行 halmos 即可。符号存储需 forge install a16z/halmos-cheatcodes。
适用场景：数学属性、溢出、访问控制等快速属性检查，CI/CD 集成，审计前验证，以及团队缺乏形式化方法经验时使用。
限制：仅做有界模型检查，无法证明需要无界循环推理的属性；复杂定点数学、幂运算或位运算可能导致 z3 超时；跨合约符号执行有限，外部调用被视为返回任意值；并非所有 EVM 操作码都支持，如符号 salt 的 CREATE2、SELFDESTRUCT 及部分预编译；分支多时可能路径爆炸；1.0 之前版本存在破坏性变更，建议固定版本。注意 assertEq 等会 revert，应使用原生 assert()。