第五章证明引擎原理与选择

Proof Orchestration（证明编排）

JasperGold 的 Proof Orchestration 自动管理多个证明引擎的调度和切换，是证明自动化的核心。

不同属性有不同的特征，适合不同的引擎。手动选择引擎需要丰富经验。Proof Orchestration 自动：

它同时启动多个引擎（Engine Race），监控各引擎的进展。当一个引擎进入 plateau（长时间没有新进展）时，编排器会：

# 设置引擎模式
set_engine_mode {K I N B L P}

# 设置时间限制
set_prove_time_limit 120s
set_prove_per_property_time_limit 30s

引擎	算法	适用场景
B / BMC	Bounded Model Checking（SAT 有界模型检测）	查找浅层 bug（短 trace 的反例）
I / Interpolation	基于 Craig Interpolation 的模型检测	中等深度属性的完整证明
K / K-Induction	K 归纳法	需要归纳证明的属性（如不变量）
N	BMC 变体（深界 BMC）	深界属性查找反例
L / PDR	Property Directed Reachability（IC3/PDR）	安全属性的完整证明，特别适合控制逻辑
P	BDD 基础引擎	小规模复杂属性
MBP	Model Based Projection	特定类型的高级证明

Engine Race 同时启动多个引擎竞争证明同一个属性，第一个完成的引擎获胜。这在 ProofGrid 环境中特别有效：

# ProofGrid 自动启用 Engine Race
set_proofgrid_mode on

当 BMC 引擎达到时间边界仍未找到反例时，产生有界证明（bounded proof）。这意味着：

状态空间爆炸是形式验证的主要挑战：

新手最常问的问题是"我应该用哪个引擎？"答案不是记住某个引擎名字，而是理解每个引擎擅长什么，然后根据问题特征选择。

1先用默认或 Tri 引擎

不指定引擎模式让工具自动选择，或用 set_engine_mode {Tri} 让 Triage 自动调度。这一步能快速解决 70-80% 的属性。

2对 remaining 属性换引擎

第一轮后剩下的属性，根据类型换引擎：控制逻辑的 fail 用 Ht/Bm 深搜，需要证明的属性用 K/I/N，特别难的用 Hp。

3对特别难的属性手动调优

少量 remaining 属性可能需要：增大时间限制、添加辅助不变量、黑盒化部分逻辑、数据路径抽象。

当你观察到以下现象时，说明遇到了状态空间爆炸：

经验法则：flop 数是状态空间的粗略指标。500 flop 以下通常容易证明；500-2000 flop 需要调优；2000 flop 以上几乎总是需要抽象和分模块验证。