Auto-sync: 2026-04-21 00:02

wiki/concepts/Formal-Verification.md

@@ -0,0 +1,38 @@
+---
+title: "Formal Verification"
+type: concept
+tags: [smart-contract, security, verification]
+sources: [blockchain-security-auditor]
+last_updated: 2026-04-20
+---
+
+## Definition
+形式化验证（Formal Verification）是使用数学方法证明智能合约正确性的技术，通过对代码进行形式化建模并验证其满足指定属性。
+
+## Methods
+- **Symbolic Execution**：符号执行，遍历代码路径
+- **Model Checking**：模型检验，验证有限状态机
+- **Theorem Proving**：定理证明，数学推导证明
+
+## Tools
+- **Certora**：以太坊智能合约形式化验证
+- **Halmos**：符号执行工具
+- **KEVM**：EVM 形式化规范
+- **Mythril**：符号执行分析
+
+## Use Cases
+- 验证协议不变量（如 total shares × price = total assets）
+- 证明访问控制逻辑正确性
+- 验证数学公式实现正确性
+- 穷举攻击路径
+
+## Limitations
+- 状态空间爆炸问题
+- 需要形式化规范（specification）
+- 工具和专家稀缺
+- 无法证明元编程安全性
+
+## Connections
+- [[Static Analysis]] ← complements ← [[Formal Verification]]
+- [[Smart Contract Security]] ← enables ← [[Formal Verification]]
+