📖 术语
🟢 通俗解释
🔰 新手
📐 形式化验证 Formal Verification
形式化验证用数学证明来确认：智能合约在每一种可能的输入下都严格按预期运行，而不只是某人碰巧试到的那几种情况。
💡
常见误解 — 「通过形式化验证」就代表合约没 bug 了？不一定！它只能证明代码遵守事先写下的那套规则。规则一旦有疏漏，真正的 bug 照样存在。
🧮 一句话讲透 —— 证明公式，而不是抽查答案
想象一场数学考试。普通的测试，好比对几道题的答案核对一遍，没发现错——听着踏实，可你并没试遍所有数字。形式化验证则是直接证明背后的公式成立，于是不管代进去哪个数字都对。放到加密货币里，这个「公式」就是一份智能合约，验证则是一口气对它所有可能的输入做推理。
⚙️ 它到底是怎么跑的
第一步，开发者写一份形式化规约：把合约必须永远遵守的规则一条条精确列出来，比如「一个资金池付出去的，绝不能超过它持有的」。接着，自动化工具用数学方法去检查代码会不会在某种情况下破坏这些规则——全程根本不用真的去运行合约。代码安全，工具就交还一份证明；不安全，工具就把那个破坏规则的具体输入原原本本指给你看。
| 步骤 | 做什么 |
|---|---|
| 📝 写规约 | 由人来写出合约绝不能违反的规则 |
| 🤖 检查 | 工具对每一种可能的输入做推理，而不是只跑那几个测试用例 |
| ✅ 结果 | 要么给出规则成立的证明，要么给出一个反例，指明哪里会出错 |
🔧 常会看到这些工具的名字：Certora Prover、Solidity 自带的 SMTChecker，以及 Coq、Isabelle、K framework 这类证明系统。Mythril 和 Manticore 是相关的分析工具。
🔒 为什么它在加密货币里这么重要
部署上链的智能合约通常不可更改——不像 App 那样能打补丁——而它手里往往攥着大笔资金。所以一个 bug 就可能意味着永久、无法追回的损失。形式化验证在这里的价值，就是能逮住一些细微的 bug 类型，比如重入攻击（reentrancy）和整数溢出（integer overflow）——这些靠随手测一下、甚至靠人工过一遍，都未必看得出来。
🤝 它替代不了审计
形式化验证和智能合约审计管的是不同的风险，所以正经项目两者都做。验证证明代码符合它的规约；人工审计问的则是另一个问题：规约本身合不合理，整体设计里有没有哪条规则都没覆盖到的弱点。只做一样，缺口就还在。
🌍 新手会在哪儿碰到它
- 📊 DeFi 审计报告 —— 在 DeFi 的安全说明里，常能看到「已通过形式化验证」或「由 Certora 验证」这样的字眼
- 🏦 MakerDAO（DAI） —— DAI 背后的核心引擎，就是用 K framework 做的形式化验证
- 🔁 Uniswap —— Uniswap 的 AMM 数学公式（x·y=k）以及 v4 的偿付能力，都用 Certora Prover 做过形式化验证
- 🛡️ 其他协议 —— Aave 等项目也在用 Certora Prover（这是厂商口径，覆盖范围的数字当作大致参考即可）
❓ 常见问题
- 「通过形式化验证」是不是就代表合约没有 bug、无法被黑？
- 不是。它只能证明代码符合事先写下的规则。如果这些规则本身不完整，或者描述错了方向，真正的 bug 照样可能漏过去。它是很有力的佐证，但不等于安全保证。
- 形式化验证和普通测试有什么不一样？
- 测试只检查少数几个示例输入，最多只能证明 bug 存在。形式化验证一次性对每一种可能的输入做推理，目标是证明：针对你写下的规则，一整类 bug 根本不会出现。
- 代码做了形式化验证，是不是就可以省掉人工审计？
- 不能。两者管的风险不一样。验证证明代码符合规约，而人工审计追问的是另一件事：规约和设计本身是否合理。靠谱的项目会两者并用。