形式化验证实战：Certora、Halmos 与 Echidna 的规约、边界与 CI 集成

测试能证明 bug 存在，却无法证明 bug 不存在。形式化验证的价值正在于此：它把「合约在所有可能的输入与调用序列下都满足某条性质」变成可被机器证明或证伪的命题。在管理数十亿美元资产的协议里，这条性质可能是「总供应量恒等于所有余额之和」，也可能是「任何人都无法提取超过自己存入的资产」。

本文按「规约表达 → 工具机制 → 边界与成本」的顺序展开：先讲清不变式怎么写，再分别拆解 Certora Prover、Halmos、Echidna 三套工具的证明方式与适用场景，最后给出验证覆盖的真实边界、CI 集成成本，以及它如何与人工审计互补。

前置：智能合约攻击面与防御体系，单元测试、模糊测试与不变量测试的工程基础。

目录

• 1. 形式化验证的定位与价值
• 2. 不变式与规约表达
• 3. Certora Prover 与 CVL
• 4. Halmos 符号执行
• 5. Echidna 属性测试
• 6. 三套工具的对比与选型
• 7. 验证覆盖的边界
• 8. CI 集成与成本
• 9. 与人工审计的配合
• 10. 工程落地建议

1. 形式化验证的定位与价值

1.1 三类验证强度

安全验证手段按强度可分三档：

关键认知是：形式化验证只能证明「代码符合规约」，不能证明「规约符合意图」。规约写错时，验证会给出虚假的安全感——这类失败在真实事故中并不罕见。

1.2 何时值得做

形式化验证的成本显著高于测试，适合的场景有明确特征：

• 核心资产逻辑（借贷、AMM、金库、桥），一处漏洞即造成不可逆损失。
• 数学性质明确的模块（舍入、精度、守恒律、单调性）。
• 升级频繁的合约，需要回归验证每次改动未破坏既有性质。
• 面向机构或监管的项目，验证报告是合规材料的一部分。

反之，UI 逻辑、一次性脚本、快速迭代的试验性合约，投入形式化验证的性价比很低。

2. 不变式与规约表达

2.1 不变式的三种类型

**不变式（invariant）**是在所有可达状态下都必须成立的性质。按作用范围可分为：

• 全局不变式：任何时刻都成立。例如 totalSupply == sum(balanceOf)。
• 转移后不变式：某操作执行后成立。例如 deposit 之后 shares > 0。
• 条件不变式：在前置条件成立时保证。例如「仅当抵押率大于阈值时允许借款」。

// 全局不变式示例：ERC-20 的供应量守恒
function invariant_TotalSupplyEqualsSumOfBalances() public view {
    uint256 sum;
    for (uint256 i = 0; i < holders.length; ++i) {
        sum += token.balanceOf(holders[i]);
    }
    assertEq(token.totalSupply(), sum, "supply mismatch");
}

2.2 规约的表达要点

写好规约比选对工具更难。几条经验：

• 从经济语义出发而非代码结构：规约应描述「用户不能凭空获利」而非「这个 if 分支走哪边」。
• 显式写出前置条件：绝大多数误报源于未声明的环境假设。
• 避免恒真规约：assert(true) 永远通过，但毫无价值。应确认规约在存在 bug 时确实会失败。
• 用小规模实例验证规约本身：先用已知有 bug 的旧版本验证规约能捕获它，再用于新版本。

// 经济语义规约：任何调用序列后，攻击者资产不得增加
rule noFreeMoney(env e) {
    uint256 before = token.balanceOf(attacker);
    method f;
    calldataarg args;
    f(e, args);
    uint256 after_ = token.balanceOf(attacker);
    assert after_ <= before, "attacker gained value";
}

3. Certora Prover 与 CVL

3.1 工作机制

Certora Prover 把 Solidity 编译为中间表示，再用 SMT 求解器验证 CVL（Certora Verification Language）规则。它的核心能力是路径完备：对每条规则，Prover 会探索所有可能的调用序列与参数组合。

Certora 验证流程：
1. 编译合约（solidity / vyper）为 IR
2. 解析 CVL 规约，生成验证条件
3. 拆分为多个 SMT 查询并行求解
4. 全部 UNSAT → 规则通过
5. 任一 SAT → 输出反例（调用序列 + 参数）

3.2 CVL 规则编写

CVL 有三类主要构件：rule（属性）、invariant（不变式）、parametric rule（任意方法调用）。

methods {
    function totalSupply() external returns (uint256) envfree;
    function balanceOf(address) external returns (uint256) envfree;
}
invariant totalSupplyIsSumOfBalances()
    totalSupply() == sumOfBalances()

// 参数化规则：任意方法执行后抵押率约束不被绕过
rule borrowRequiresCollateral(env e, uint256 amount) {
    require e.msg.sender != 0;
    uint256 healthBefore = healthFactor(e.msg.sender);
    borrow(e, amount);
    assert healthBefore > 1e18 => healthFactor(e.msg.sender) >= 1e18;
}

envfree 标注表示该函数不依赖 msg.sender、msg.value 等环境变量，可以让 Prover 跳过环境建模，显著加速。

3.3 反例的价值

Certora 输出反例时给出完整的调用序列与参数，这是它最有价值的部分：反例往往直接暴露了开发者没想到的状态组合。工程上应把每条反例固化为回归测试用例，避免修复后再次退化。

4. Halmos 符号执行

4.1 机制与定位

Halmos 是 Foundry 生态里的符号执行引擎：它复用 Foundry 的测试框架，把测试函数的参数当作符号值而非具体值，用 SMT 求解器判定所有分支下的断言是否成立。

// 与普通 Foundry 测试写法一致，但参数被符号化
function check_DepositRedeemNeverProfits(uint256 assets) public {
    // assets 是符号值，Halmos 会检查所有可能的取值
    vm.assume(assets > 0 && assets < 1e30);
    uint256 shares = vault.deposit(assets, address(this));
    uint256 back = vault.redeem(shares, address(this), address(this));
    assert(back <= assets);
}

运行方式与 Foundry 测试一致，只需把 test 前缀改为 check 并用 halmos 命令执行。

4.2 适用与限制

Halmos 的优势是「零迁移成本」：已有的 Foundry 测试稍加改动即可符号化执行，非常适合作为形式化验证的入门与日常回归。

4.3 实用技巧

• 用 vm.assume 缩小输入空间：不加约束时求解器会在无意义的边界值上耗时。
• 展开循环：--loop 4 之类参数控制展开次数，超过即视为不可判定。
• 限制外部调用：对未建模的合约调用，用 vm.mockCall 固定行为。
• 分批验证：把大函数拆成小函数分别符号执行，降低求解复杂度。

5. Echidna 属性测试

5.1 属性测试的机制

Echidna 是基于属性的模糊测试器：开发者定义不变量，Echidna 随机生成调用序列并尝试破坏它。与纯随机 fuzz 不同，Echidna 会用覆盖率反馈与语料变异提升探索效率。

contract VaultInvariants is Vault {
    // Echidna 会自动调用任意函数序列，检查该断言
    function echidna_supply_conserved() public view returns (bool) {
        return totalSupply <= MAX_SUPPLY;
    }

    // 带前置条件的属性
    function echidna_no_unauthorized_withdraw() public view returns (bool) {
        return address(this).balance >= totalDeposits;
    }
}

5.2 配置与运行

# echidna.yaml
testMode: assertion
testLimit: 50000
seqLen: 100
shrinkLimit: 5000
coverage: true

关键参数是 seqLen（调用序列长度）：很多漏洞只在多步序列后出现，序列过短会漏检。shrinkLimit 控制反例最小化，把长序列压缩成最短复现路径。

5.3 与单元测试的差别

Echidna 与形式化验证的差别在于：它不保证完备，但运行成本极低，适合作为 CI 中的常驻检查。

6. 三套工具的对比与选型

6.1 能力矩阵

6.2 组合使用

实务中最有效的组合是三层叠加：

第一层 Echidna    每次提交运行，快速发现明显不变量破坏
第二层 Halmos     每日或每次发布运行，符号化验证关键函数
第三层 Certora    发布前运行，对核心模块做路径完备证明

三层覆盖的成本递增，但每一层都能捕获上一层漏掉的问题类型。

7. 验证覆盖的边界

7.1 环境假设的代价

形式化工具必须对「合约之外的世界」做假设：预言机价格如何变化、外部合约如何响应、区块时间如何推进。假设一旦放宽，求解复杂度爆炸；假设一旦收紧，验证结论就不再覆盖真实场景。

// 常见环境假设：价格变化幅度受限
rule liquidationAlwaysSolvent(env e) {
    require priceChangePct <= 30;   // 假设单次价格波动不超过 30%
    // ... 验证清算逻辑
}

这条规则证明的是「价格波动 30% 以内时清算安全」，不是「清算永远安全」。报告与文档必须把假设写清楚，否则会误导读者。

7.2 循环与递归

SMT 求解器无法处理无界循环。工具的处理方式有三种：循环展开到固定次数、抽象为不变式、或直接放弃该路径。任何涉及无界循环的逻辑（批量处理、递归清算）都会在验证中留下盲区。

7.3 外部调用的建模

call 到未建模的合约时，工具通常假设「返回任意值」，这会产生大量误报；若用 mock 固定返回值，则失去对该交互的覆盖。合理做法是对关键外部依赖（预言机、代币）单独建模，其余用受约束的抽象。

7.4 盲区清单

• 编译器与 EVM 语义：验证在 IR 层进行，编译器 bug 与 EVM 层语义不在覆盖范围。
• 代理与存储布局：升级代理的实际存储布局常与实现合约的假设不一致，需要专门的布局验证。
• 经济假设：预言机可信、套利者理性等假设无法被证明。
• gas 与 DoS：形式化工具一般不建模 gas 消耗，无法发现「逻辑正确但会 out of gas」的问题。
• 密码学原语：哈希与签名的性质被当作公理，不验证其实现。

8. CI 集成与成本

8.1 CI 流水线设计

# 分层的 CI 设计
stages:
  - test:      forge test                    # 秒级
  - fuzz:      forge test --fuzz-runs 5000   # 分钟级
  - echidna:   echidna-test . --config ...   # 分钟级
  - halmos:    halmos --function check_      # 十分钟级
  - certora:   certoraRun ...                # 小时级，仅在发布分支

关键是按成本分层：快速检查每次提交都跑，昂贵验证只在合并到发布分支或打标签时跑。

8.2 成本构成

人力成本远高于工具成本：写规约、理解反例、调整假设，都需要既懂业务又懂验证的工程师。

8.3 常见失败模式

• 规约恒真：规则写得太弱，永远通过，产生虚假安全感。
• 假设过强：require 条件把真实场景排除在外，验证结果无意义。
• 超时被忽略：求解超时（timeout）被当成通过，实际是未验证。
• 规约腐化：合约升级后规约未同步，验证仍在跑但已不对应新逻辑。

9. 与人工审计的配合

9.1 分工

形式化验证与人工审计解决的是不同问题：

形式化验证不能替代审计，但可以显著提高审计的效率：审计员可以把精力放在「规约之外」的风险上。

9.2 协作流程

1. 审计员提出关键不变量 → 团队写成规约
2. 形式化验证运行 → 反例交给审计员分析
3. 审计员发现的设计缺陷 → 补充为新规约
4. 修复后回归验证 → 确认未引入新问题
5. 最终报告同时包含审计发现与验证结论

把「审计发现的每个高危问题」都转化为一条形式化规约，是最有效的知识固化方式。

10. 工程落地建议

10.1 从哪开始

不建议一开始就追求核心合约的完备证明，更现实的路径是：

1. 先写不变量测试：用 Foundry 的 invariant 测试建立基础，成本最低。
2. 引入 Echidna：把不变量测试迁移为属性测试，获得自动序列探索能力。
3. 关键函数符号化：用 Halmos 对数学密集函数做符号执行。
4. 核心模块形式化：对金库、清算、权限模块上 Certora。
5. 纳入 CI：分层执行，把验证变成持续过程而非一次性项目。

10.2 组织与流程

• 规约与代码同仓：规约随合约一起版本管理、一起评审。
• 反例即测试：每个反例固化为回归用例。
• 假设显式化：所有环境假设写在规约文件顶部并纳入评审。
• 验证报告公开：把验证结论与假设边界同时公开，避免误导用户。
• 超时视为失败：CI 中不允许「超时通过」，必须调整规则或显式标注未验证。

10.3 速查表与一句话记忆

一句话记忆：形式化验证证明的是「代码符合规约」，规约的边界与假设才是真正的安全边界。

延伸阅读

• 智能合约攻击面、防御体系与审计流程
• Foundry 单元测试、模糊测试与不变量测试
• 标准接口的隐含假设与组合风险
• 代理升级的存储布局与初始化风险
• 合约开发流程与工程化实践
• Web3 区块链专题 — 区块链 Web3 专题