---
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]]