39 lines
1.1 KiB
Markdown
39 lines
1.1 KiB
Markdown
---
|
||
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]]
|
||
|