用途：Halmos（a16z/halmos）是 EVM 智能合约的符号测试工具，用符号执行加 SMT 求解器替代随机模糊测试，在给定边界内验证所有可能输入。
主要能力：采用 Solidity/Foundry 前端，编写 check_ 或 invariant_ 前缀测试，类似模糊测试写法；支持符号化构造函数参数；支持对调用序列做不变量测试，可配置 --invariant-depth 与 frontier states；可配置求解器（Yices、cvc5、Bitwuzla），支持超时、--solver-threads、--solver-command。
使用方式：通过 CLI 调用，可用 --contract/--function 指定目标，使用 halmos.toml 配置，支持 @custom:halmos 注解；setUp 与 cheatcode 部分涉及符号化构造函数参数及 svm.createUint256、createAddress、createBytes 等，并涉及 halmos-cheatcodes。
适用场景：需要比模糊测试更强保证的合约验证，尤其是检查断言、revert 条件、动态类型与不变量。
限制：资料未提供具体安装命令、版本、收费、性能数据与平台支持细节；符号执行与 SMT 求解可能受边界与求解器能力限制，具体以官方文档为准。