3、模型检测入门：状态空间、迁移系统、时态逻辑（LTL/CTL）、模型检测算法概述
模型检测，说白了就是「穷举验证」。你写了一个智能合约，想知道它有没有 bug？模型检测会遍历所有可能的状态，告诉你「有」或「没有」。我最早接触这玩意儿是在做跨链桥安全审计的时候，那会儿合约状态多到爆炸，手动测试根本测不完。后来发现，模型检测才是治本的办法。
3.1 状态空间：你的合约到底有多少种可能？
状态空间，就是系统所有可能状态的集合。拿一个简单的计数器合约举例：
contract Counter {
uint public count;
function inc() public { count += 1; }
function dec() public { count -= 1; }
}如果 count 是 256 位的整数，那状态空间就是 2^256 种可能。嗯，这数字大到离谱。实际做模型检测时，我们不会真的枚举所有 2^256 个状态，而是做抽象——比如把 count 限制在 0 到 3 之间，或者用符号化表示。
关键点：状态空间的大小决定了模型检测能不能跑完。我见过一个项目，状态空间 10^20 量级，用 BDD（二叉决策图）硬是压到了可处理的范围。抽象和符号化是两大法宝。
状态空间里每个状态，都是一个快照。比如：
(count=0, owner=0x123...)(count=1, owner=0x123...)(count=0, owner=0x456...)
每个变量取值的组合，就是一个状态。状态空间就是这些组合的全体。
3.2 迁移系统：状态之间怎么跳？
有了状态，还得知道状态之间怎么变。迁移系统就是干这个的。它由三部分组成：
- 状态集合 S：所有可能的状态
- 初始状态集合 I：合约部署时的状态
- 迁移关系 R：从状态 s 到状态 t 的跳转规则
举个例子，上面的计数器合约，迁移关系可以写成：
inc: (count == n) → (count == n+1)
dec: (count == n) → (count == n-1)每个函数调用都是一条迁移边。你想想看，如果合约里有 require 语句，那迁移关系就带条件了：
withdraw(amount):
require(balance >= amount);
balance -= amount;只有满足 balance >= amount 的状态，才能触发这条迁移。
个人经验：我在审计一个 DeFi 协议时，发现它的迁移关系里有个「幽灵状态」——某个条件永远无法满足，导致一段代码永远执行不到。模型检测一跑，直接暴露了这条死代码。手动 review 根本看不出来。
3.3 时态逻辑：怎么描述「永远不出事」？
状态空间和迁移系统描述的是「系统长什么样」。但我们要验证的是「系统行为对不对」。时态逻辑就是用来描述行为性质的。
3.3.1 LTL（线性时态逻辑）
LTL 假设时间是一条线，每个时刻只有一个后继。常用的操作符：
- G p：全局成立（Globally），p 在所有未来状态都成立
- F p：最终成立（Finally），p 在某个未来状态成立
- X p：下一个状态成立（neXt）
- p U q：p 一直成立直到 q 成立（Until）
举个例子，验证「合约永远不会被重入攻击」：
G (call_external → (lock == true))意思是：任何时候，只要发起外部调用，锁必须是 true。这就是一个典型的 LTL 性质。
避坑指南：我曾经写过一个 LTL 公式 G (F paid)，意思是「最终一定会付款」。结果模型检测说这个性质不成立。我查了半天，发现合约里有个分支路径可以无限循环，永远不执行付款逻辑。LTL 能捕捉这种「无限拖延」的问题，手动测试很难发现。
3.3.2 CTL（计算树逻辑）
CTL 和 LTL 最大的区别：CTL 考虑的是「分支时间」，每个时刻可能有多个后继。操作符前面必须加路径量词：
- A：所有路径（All）
- E：存在某条路径（Exists）
比如：
- AG p：所有路径上，p 全局成立
- EF p：存在某条路径，最终 p 成立
- AF p：所有路径上，最终 p 成立
- EG p：存在某条路径，p 全局成立
举个例子，验证「存在一条路径可以让合约自毁」：
EF (selfdestruct_called == true)如果模型检测返回 true，说明确实有办法触发自毁。如果返回 false，说明自毁函数永远无法被调用——可能是权限控制太严了。
| 特性 | LTL | CTL |
|---|---|---|
| 时间模型 | 线性（单路径） | 分支（多路径） |
| 路径量词 | 隐含（所有路径） | 显式（A/E） |
| 表达能力 | 擅长描述「沿路径」的性质 | 擅长描述「分支选择」的性质 |
| 典型应用 | 公平性、活性 | 可达性、安全性 |
我的建议：做智能合约安全验证时，我一般先用 CTL 查「可达性」——比如某个危险函数能不能被调用。再用 LTL 查「活性」——比如某个承诺最终会不会兑现。两者互补，缺一不可。
3.4 模型检测算法：机器是怎么遍历的？
算法层面，模型检测的核心就是「状态空间搜索」。但直接暴力搜索肯定不行，得用点技巧。
3.4.1 显式状态模型检测
最朴素的方法：把状态一个一个列出来，然后 BFS 或 DFS 遍历。每个状态存到哈希表里，避免重复访问。
visited = set()
queue = [initial_state]
while queue:
s = queue.pop()
if s in visited: continue
visited.add(s)
for t in successors(s):
if property_holds(t):
queue.append(t)
else:
report_counterexample(t)这个方法的问题很明显：状态一多就炸了。我试过跑一个 10 个变量的合约，状态空间 2^10 = 1024，还行。但 20 个变量就是 100 万，直接内存溢出。
3.4.2 符号化模型检测
符号化方法用 BDD（二叉决策图）或 SAT/SMT 求解器来表示状态集合和迁移关系。不存具体状态，存布尔公式。
比如状态 (count=0) ∨ (count=1) 可以用一个 BDD 节点表示。迁移关系 inc 可以写成 count' = count + 1 的布尔公式。然后通过不动点计算来验证性质。
核心思想：不动点计算。比如验证 AG p（所有路径上 p 都成立），算法会从「所有满足 p 的状态」出发，反复去掉那些能一步走到非 p 状态的状态，直到收敛。收敛时的状态集合，就是 AG p 成立的最大区域。
3.4.3 有界模型检测（BMC）
BMC 是另一种思路：我不遍历所有状态，我只展开 k 步，然后检查这 k 步内有没有违反性质。用 SAT 求解器来解。
for k = 1 to MAX_DEPTH:
formula = (初始状态) ∧ (迁移^1) ∧ ... ∧ (迁移^k) ∧ (¬性质在第k步)
if SAT(formula) == true:
return counterexample of length kBMC 的好处是快，坏处是只能找到「有限步」的反例。如果性质在 100 步之后才违反，而你的 k 只设到 50，那就漏了。
注意：BMC 不能证明性质成立，只能证明「在 k 步内没发现反例」。我见过有人拿 BMC 当完整验证用，结果上线后被攻击了——攻击路径需要 200 步，而他的 BMC 只跑了 50 步。完整验证还得靠符号化模型检测或归纳法。
3.5 实际应用中的选择
做智能合约形式化验证时，我一般这样选：
- 小规模合约（状态 < 10^6）：显式状态模型检测，简单直接
- 中等规模（状态 10^6 ~ 10^12）：符号化模型检测，用 BDD 或 SMT
- 大规模（状态 > 10^12）：BMC 加抽象，或者用归纳法
工具方面，我常用 NuSMV 做符号化模型检测，用 CBMC 做有界模型检测。对于 Solidity 合约，可以先用 Slither 转成中间表示，再喂给这些工具。
最后说一句：模型检测不是银弹。状态空间爆炸是永远的敌人。但如果你能做好抽象、选对逻辑、用对算法，它绝对是你安全工具箱里最锋利的一把刀。我每次审计关键合约，都会先跑一遍模型检测——哪怕只跑出几个反例，也比上线后被人跑出反例强得多。