Halmos v0.3.0 版本发布亮点

Halmos v0.3.0 发布啦！

Halmos 是 EVM 智能合约的符号测试工具，它使用符号执行来帮助查找错误和验证合约行为。自 v0.2.0 以来，我们一直专注于使 halmos 在实际错误查找方面更有效，而不仅仅是形式验证。

此版本延续了这一方向，支持状态不变量测试，这是我们用户最需要的功能。为此，我们还添加了一些支持功能，包括覆盖率报告、性能改进、更好的求解器支持等等。

状态不变量测试

除了无状态的 check_ 测试之外，Halmos 现在还将查找以 invariant_ 前缀开头的测试。当测试合约包含 invariant_ 测试时，halmos 将自动高效地：

• 发现目标合约（通常是在 setUp() 期间部署的合约）
• 发现目标函数（目标合约的公共、状态修改函数）
• 探索通过调用目标函数的所有可能序列（最多 --invariant-depth，默认为 2）产生的状态
• 对于每个可达状态，断言所有不变量并报告任何失败

查看 a16z/halmos/examples/invariants 以开始使用。

覆盖率报告

使用 --coverage-output lcov.info，halmos 以标准 lcov 格式输出覆盖率信息。可以使用 genhtml 将其呈现为 html，或者使用像 Coverage Gutters 这样的扩展在 VSCode 中可视化。

火焰图

你现在可以使用 --flamegraph 调用 halmos。在不变量测试期间，这将生成 call-flamegraph.svg，这是一种方便的方式来可视化到目前为止探索的所有调用序列。

生成的 svg 是交互式的，因此你可以搜索 FAIL 以可视化导致反例的序列。

更快的 interpreter

我们彻底 优化了 EVM 解释器 循环，从而使执行速度提高了 32 倍。

更好的 solver 支持

我们一直支持第三方 SMT 求解器，通过

--solver-command <path/to/solver solver-args>

但这有点难用。你需要自带 求解器 （例如，自己安装或构建）。但最重要的是，你需要知道使其工作的正确咒语。例如，除非你使用 --produce-models 调用 bitwuzla，否则它不会产生反例，并且除非你使用 --smt2-model-format 调用 yices，否则 halmos 无法解析 yices 产生的反例。

现在你只需给出要使用的 求解器 的名称（例如 --solver cvc5、--solver yices、--solver z3 等），halmos 就会将其转换为完整的 求解器 命令。Halmos 将：

• 如果你已经安装了 求解器 （在你的 PATH 或 halmos 缓存中），则找到该 求解器
• 如果你没有安装 求解器，则提供安装它的选项并将其保存在 halmos 缓存中
• 使用正确的参数调用它

较低级别的 --solver-command 选项仍然可供高级用户使用，但 –solver 是大多数用户的推荐选项。

感谢 Josselin 的建议！运行 halmos --help 以查看具有支持配置的 求解器。

Yices 是新的默认 solver

利用前面提到的改进的 求解器 支持，我们认为对于大多数用户来说，yices 比 z3 更好。它通常快 3-5 倍，但偶尔可以快几个数量级。

solx 支持

如果你错过了：solx 是一个基于 LLVM 的实验性 Solidity 编译器。它可以作为 solc 的直接替代品使用，并且可以与 Foundry 一起使用，这意味着它也可以与 halmos 一起使用。

要试用它：

1. 从 GitHub 发布页面 获取最新版本的 solx。
2. 创建一个 foundry profile：

## foundry.toml

[profile.solx]
solc_version = "/usr/local/bin/solx"

3. 使用 solx profile 调用 halmos：

FOUNDRY_PROFILE=solx halmos

在 Matter Labs 的 solx 发布博客 帖子中了解更多信息。

Cheatcode 支持

我们添加了通过以下 作弊码 从环境变量和 .env 文件中提取值的支持：

• envInt(string key)
• envBytes32(string key)
• envAddress(string key)
• envBool(string key)
• envUint(string key)
• envString(string key)
• envBytes(string key)

我们还支持数组版本（例如 envAddress(string key, string delimiter) returns (address[]) 和带有回退值的 envOr 版本（例如 envAddress(string key, address fallback)。

此外，我们还支持 随机 系列的 作弊码：

• randomAddress()
• randomBool()
• randomBytes()
• randomBytes4()
• randomBytes8()
• randomInt()
• randomInt(uint256 bits)
• randomUint()
• randomUint(uint256 min, uint256 max)
• randomUint(uint256 bits)
• setArbitraryStorage(address target)

如果你想编写既可以用作 foundry fuzz 测试又可以用作 halmos 符号测试的测试，这些 作弊码 很有用。在 foundry book 中了解更多信息。 特别感谢 Jayakumar 的贡献！

进度 indicators

我们现在显示实时进度 indicators，以了解 halmos 在长时间会话中的工作情况：

• 在路径探索期间，你将看到 ops/s（已 解释 的指令）的数量以及已完成路径的数量
• 在断言 求解 期间，你将看到已 求解 的查询数量和剩余的查询数量

How to upgrade

到目前为止，安装和升级 halmos 最简单的方法是使用 uv：

1. install uv
2. 运行 uv tool install --python 3.13 halmos
3. 运行 uv tool upgrade halmos

• 原文链接： a16zcrypto.com/posts/art...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～