---
title: "Invariant Verification"
type: concept
tags: [smart-contract, security, testing]
sources: [blockchain-security-auditor]
last_updated: 2026-04-20
---

## Definition
不变量验证（Invariant Verification）是通过属性驱动测试（Property-Based Testing）验证智能合约关键属性始终成立的方法。

## Invariant Examples
- `totalShares × pricePerShare = totalAssets`（资产管理器）
- `pool.balance ≥ sum(userBalances)`（余额不变量）
- `onlyOwner can upgrade`（权限不变量）
- `mint/Burn pair maintains supply`（代币供应不变量）

## Tools
- **Echidna**：Property-based fuzzing
- **Foundry/Forge**：invariant testing
- **Medusa**：模糊测试

## Process
1. 定义协议不变量
2. 编写 invariant 测试用例
3. 使用模糊测试生成攻击输入
4. 验证 invariant 是否被破坏
5. 迭代修复直至测试通过

## Limitations
- 只能测试已想到的不变量
- 模糊测试覆盖率有限
- 复杂状态空间难以穷举
- 需要领域专业知识定义不变量

## Connections
- [[Formal Verification]] ← is_formal_version_of ← [[Invariant Verification]]
- [[Echidna]] ← provides ← [[Invariant Verification]]
- [[Smart Contract Testing]] ← includes ← [[Invariant Verification]]