合约审计和形式化验证在做什么

全文分三层：

1. 通俗理解：体检、压力测试和数学证明
2. 实际用处：主流工具、为什么"审计过"仍被盗、怎么读审计报告
3. 原理与工程要点：不变量怎么写、形式化验证的边界

第一层：通俗理解

1.1 四种检查

1.2 "什么算对"是最难的

所有手段都需要回答一个问题：这个合约应该满足什么性质？比如：

• "所有用户的存款加起来，永远不超过合约实际持有的代币"；
• "只有所有者能调用升级函数"；
• "任何人取出的钱，不能多于他存入的加上应得的利息"。

把这些性质写清楚，往往比找 bug 本身更有价值。

第二层：实际用处

2.1 主流工具

2.2 为什么"审计过"仍被盗

2.3 怎么读审计报告

• 看范围：审计了哪些文件、哪个提交（commit hash）？和线上部署的字节码一致吗？
• 看发现：高危、中危问题各有几个？修复状态是"已修复""已确认但不修"还是"有争议"？
• 看审计方：是否独立；同一项目是否有多家审计、是否有漏洞赏金计划（见《负责任披露与漏洞赏金》）；
• 看时间：审计是多久以前的？之后有没有升级过？

第三层：原理与工程要点

3.1 不变量测试

不变量是"无论用户怎样调用、按什么顺序调用，都必须始终成立"的性质。测试框架会随机生成大量调用序列，每一步之后检查不变量：

// 不变量：合约实际持有的代币 ≥ 记录的所有用户余额之和
function invariant_solvent() public {
    assertGe(token.balanceOf(address(vault)), vault.totalDeposits());
}

好的不变量来自对业务的理解：

3.2 形式化验证

把合约代码和性质都翻译成数学逻辑，用求解器证明"对于所有可能的输入和状态，性质都成立"；如果不成立，求解器会给出一个具体的反例。

它比测试强在穷尽：测试只能试有限多种情况，证明覆盖全部。但它有明确的边界：

• 只证明你写下的性质：漏写了一条重要性质，证明照样"通过"；
• 模型假设：比如假设外部合约行为正常，而真实世界里外部合约可能是攻击者写的；
• 成本高：需要专门的人才，复杂合约可能证明不出来（超时）。

3.3 一个推荐的流程

1. 写清楚规格：合约应该做什么、不应该做什么、有哪些不变量；
2. 开发时持续跑静态分析和单元测试；
3. 写不变量测试，长时间跑模糊测试；
4. 对核心逻辑做形式化验证（如果条件允许）；
5. 多家独立审计；
6. 上线后：漏洞赏金、实时监控、暂停开关、限额（见《Fail-closed》）。

每一步都只能降低风险，不能消除风险。"纵深防御"的意思是：前面几层漏掉的问题，后面几层还有机会抓住或者限制损失。

总结