形式化验证工具全景选型指南

本文档整理了工业级形式化验证工具的全景对比，按重要程度排列分类维度，并给出三张核心对照表（能力矩阵、信任与合规、落地风险）以及各工具逐条说明。

判断标准：「工业验证过」指满足至少一条——① 被安全认证标准（DO-178C/ISO 26262/IEC 61508/CC EAL）认可并有鉴定包；② 在生产系统中长期运行且有公开事故/漏洞发现记录；③ 由商业公司持续维护并出售支持；④ 开源但有大厂 CI 常驻。

分类维度总览（按重要程度排列）

第一组：身份与定位（决定它能不能进候选池）

第二组：能力与强度（决定它能证什么）

第三组：信任与合规（决定结论能不能对外说）

第四组：工程落地（决定它能不能活过两年）

表 A：能力矩阵（给技术负责人看）

列：层位 · 输入语言 · 方法流派 · 结论强度 · 性质类 · 并发 · unsafe · 注解负担 · 规模上限

第 0 层：求解器与证明引擎

第 1 层：交互式定理证明器

第 2 层：演绎式程序验证（auto-active / SMT）

第 3 层：模型检验

第 4 层：抽象解释与无假阴性静态分析

第 5 层：硬件与 RTL 形式验证

第 6 层：已验证编译器与工程件

表 B：信任与合规（给安全/认证/审计看）

列：信任基 · 编译链覆盖 · 认证背书 · 证据形态 · 维护方与许可

表 C：落地风险（给项目经理看）

列：工业案例 · 活跃度/是否停更 · 证明回归 · 人才曲线 · 成本 · 明确不适用场景

工具逐条速查（按技术流派分组）

求解器与证明引擎

• Z3 (2006, Microsoft Research, MIT许可) — SMT求解器事实标准，Herbrand Award 2019。几乎所有auto-active工具都靠它。但本身不产生「数学证明」，只给出可满足性判定。
• CVC5/CVC4 (2011/2021, Stanford+UIowa+NYU) — Z3的替代/互补后端。学术与部分工业流程双后端。
• Alt-Ergo (2007, OCamlPro) — 专为程序验证调优的SMT。Frama-C、GNATprove的默认后端之一。
• MiniSat/Glucose/CaDiCaL (2003+, 开源) — SAT求解内核。BMC/EDA工具的底层引擎。

交互式定理证明器

• Coq (1989, Inria+社区) — 构造演算，小内核可独立检查。CompCert、JavaCard EAL7(12万行Coq)、Fiat-Crypto、RISC-V规范、四色定理/Feit-Thompson。可提取代码。
• Isabelle/HOL (1986, Cambridge+TUM+Data61) — 高阶逻辑，LCF小内核。seL4(20万行起)、AWS Nitro隔离引擎(25万行证明)、WebAssembly语义。
• HOL4/HOL Light (1985/1998) — 高阶逻辑极小内核。seL4二进制等价证明、Graviton2密码优化、AMD Zen4 TLB同步验证。
• Lean 4 (2013, 开源社区+云厂商) — 依赖类型。数学库最猛；工程侧仍在爬坡。内置编译器带GC运行时，不适合裸系统代码提取。
• PVS (1992, SRI International) — 高阶逻辑+类型判定。NASA大量使用(航天器需求验证)，航空标准常客。
• ACL2 (1997, UT Austin+社区) — 一阶逻辑自动化强。AMD/Intel用其验证浮点单元与微码。

演绎式程序验证（auto-active / SMT）

• SPARK 2014+GNATprove (2014, AdaCore+Capgemini) — Ada子集，霍尔逻辑+Why3+多后端SMT。最成熟的工业路线之一：Eurofighter Typhoon、Rolls-Royce Trent、Muen分离内核、NVIDIA安全固件。可在DO-178C A级流程中替代部分单元测试。「证明跟着代码走」在工业界的标杆。
• Dafny (2008, MSR+开源) — 自有语言可编译到C#/Java/Go/JS/Python。IronFleet/Ironclad全栈验证内核+驱动+密码库+分布式系统。
• F* (2012, MSR+INRIA) — 证明导向编程+提取无GC C/汇编。唯一真正进生产基础设施的提取路线：HACL*(Firefox 57起/Linux内核lib/crypto/WireGuard/Python hashlib)、EverParse(Azure/Hyper-V报文解析)、ElectionGuard、Tezos。
• Verus (2024 SOSP'24, MSR+AWS+社区) — Rust子集，auto-active+Z3，支持unsafe与并发模块化推理。AWS Nitro Enclaves核心原语、IronKV、Atmosphere OS、Asterinas vostd(CertiK合作)。能力最强但最年轻，生态仍在快速变。
• Frama-C WP/Eva (2008, CEA+工业联盟) — C代码契约验证(ACSL标注)。法国核能/航空/汽车。WP:霍尔逻辑+SMT全称；Eva:抽象解释。
• Why3 (~2010, INRIA) — 验证条件生成器+多后端编排。GNATprove/Creusot的中间层。
• Prusti (2018, ETH) — Rust→Viper/Silver，基于权限的分离逻辑。学术活跃，工业落地有限。
• Creusot (~2020, INRIA) — Rust→Why3，Pearlite规约语言。亮点是&mut的prophecy编码。
• Aeneas (~2020, MSR) — Rust MIR→纯函数式模型(Lean/F*)后再手证。微软SymCrypt已验证SHA-3/ML-KEM并公开产物。
• KeY (1990s, 社区, GPLv2) — Java演绎式验证器，基于动态逻辑的相继式演算，实现前向符号执行。结合auto-active和细粒度交互证明，支持在源代码级别调试证明。验证了TimSort等复杂Java代码。开源纯Java实现，跨平台。适合教学和复杂代码验证。
• OpenJML (2000s, 社区, 开源) — Java Modeling Language (JML)的参考实现，auto-active路线。在Java代码中用JML注解写契约（requires/ensures/maintaining），通过SMT求解器自动验证。有Eclipse插件和VSCode扩展。用于高校教学和小型项目研究。不支持大型工业项目和并发验证。
• Gospel/Cameleer (2010s, 社区, 开源) — Gospel是专为OCaml设计的行为规范语言，用契约式风格在.mli文件中定义前置条件、后置条件、不变式，语义基于分离逻辑；Cameleer是Gospel的演绎验证后端，将OCaml+Gospel规约翻译为Why3，再用SMT求解器自动验证。活跃开发中，适合OCaml项目的契约验证。
• coq-of-ocaml (2010s, 社区, 开源) — 将OCaml代码翻译为Coq(Rocq)代码的翻译器。支持函数式核心、类型定义、单子程序、模块、函子，对GADTs和多态变体提供部分支持。工业案例：Tezos区块链约10万行OCaml代码的验证（内部错误缺失、向后兼容性、不变式保持、序列化正确性）。适合需要绝对正确性的OCaml核心组件验证。
• gospel-rtac (2010s, 社区, 开源) — 基于Gospel规范，用PPX机制将规约自动翻译为类型安全的OCaml运行时检查代码，在函数入口/出口、循环边界注入校验逻辑。检查器本身经过Coq或Isabelle/HOL元理论证明，确保健全性。适合需要运行时保证的OCaml项目。

模型检验

• TLA+/TLC/PlusCal (1999, 社区+TLAF/Linux Foundation) — 并发与分布式协议设计级验证。工业应用最完整的协议验证案例集：AWS DynamoDB/S3/EBS、Azure Cosmos DB、Intel/Microsoft/PingCAP(Raft)。唯一获此地位的模型检验工具。可证liveness。
• Apalache (~2019, Informal Systems) — TLA+的符号模型检验(SMT)。能处理比TLC大得多的状态空间。
• TLAPS (2000s) — TLA+的演绎证明补TLC。主要覆盖safety，liveness支持不完整。
• SPIN/Promela (1989, 社区) — 协议一致性与并发错误。NASA火星探测器(1996发射前纠错)、Lucent 5ESS、IEEE 802.11/蓝牙协议族验证。唯一获ACM软件系统奖的模型检验器。
• NuSMV/nuXmv (1999/2014, FBK) — 符号模型检验(CTL/LTL)。工业控制、轨道交通、安全协议。
• UPPAAL (1995, Aalborg+Uppsala) — 时间自动机(实时系统)。汽车电子、Bang & Olufsen音频协议(著名bug发现案例)。
• Alloy/Analyzer (2000, MIT) — 结构模型的轻量穷举分析。设计早期快速找反例。
• CBMC (~2001, Diffblue+社区) — C/C++有界模型检验。AWS FreeRTOS验证版、s2n-tls、医疗/航空嵌入式。位精确、反例可读。
• Kani (2021, AWS) — Rust版CBMC(MIR→goto-program)。AWS生产CI常驻，已在开源项目发现未知bug。零注解起步。
• ESBMC/SeaHorn/KLEE/SymCC (2011/2015/2008+) — C/C++符号执行与有界验证。嵌入式与竞赛场景。
• Loom/Shuttle/model-checker-rs (近年) — Rust/C11内存模型级交错枚举。内核内存屏障验证必用。
• herd7 (近年) — 验内存模型本身(x86-TSO/ARMv8/LKMM/PTX)。Linux自己的LKMM就是用herd7形式化的。
• StateRight (近年, 社区, 开源) — Rust显式状态模型检查器。用Rust代码定义State/Action类型并实现Model trait，调用spawn_dfs()/BFS进行穷举状态空间搜索。擅长共识/选举/复制状态机/缓存一致性/消息传递协议验证，支持safety(invariant)和liveness(LTL)性质检查，输出最短反例轨迹。提供actor运行时，同一份代码既能模型检查也能在真实网络中运行。内置linearizability/sequential consistency tester。短板：状态爆炸时需手工抽象（如将"任意任期"压成"相等/不等/大一格"三类），量化性质表达笨重，社区规模较小。

抽象解释与静态分析

• Astrée (2003, AbsInt/dSPACE) — 证明C程序无运行时错误与数据竞争。空客电传飞控(A340/A380级别，50万行可分析、误报近零)。DO-178C/ISO 26262/EN 50128鉴定包。
• Polyspace Code Prover (1998, MathWorks) — 同Astrée，Simulink/Embedded Coder生态。汽车/航空/核电主流。
• aiT/StackAnalyzer (2000s, AbsInt) — WCET与栈用量上界分析(二进制级)。丰田非预期加速调查中被引用为工业基准。
• RuleChecker/Coverity/LDRA Testbed (各异) — MISRA/CERT规则+单元覆盖+工具鉴定。车规/航电认证流水线的日常件。

硬件与 RTL 形式验证

• JasperGold (2010s, Cadence) — 属性验证、CDC、低功耗、安全、等价。SoC签核主流。
• VC Formal/Formality/SpyGlass Formal (长期, Synopsys) — RTL属性验证/RTL-to-门级等价/CDC-复位签核。ASIC/SoC流程必备。
• Questa Formal (长期, Siemens EDA) — 断言验证，仿真-形式统一平台。与UVM生态整合最好。
• OneSpin 360-DBV (2014, Siemens) — 高端形式验证。金融/安全芯片、侧信道与硬件木马。
• Yosys+SymbiYosys (2012+, 开源) — 开源形式验证栈。FPGA与开源CPU流程主力。rIC3(2024国际硬件模型检测竞赛双赛道第一)。
• SCADE Suite/Design Verifier+Lesar (1990s, Ansys) — 模型驱动开发+模型级形式验证，直接出DO-178C A级代码。空客电传飞控核心库。
• Simulink Design Verifier (2000s, MathWorks) — 模型级性质证明与测试生成。汽车/航空MBD流程标配。

已验证编译器与工程件

• CompCert (2006, Inria+AbsInt) — 已证语义保持的C编译器。Clight子集→PowerPC/ARM/x86/RISC-V。首个工业级已证编译器；AbsInt提供认证包；CertiKOS/mC2的编译链。
• Vale (~2015, MSR) — 在F*里直接验证手写汇编。Tezos密码实现、Hyper-V边界；内核入口/上下文切换的正解。
• Cryptol+SAW (~2004/~2014, Galois→Amazon) — 密码算法规范与实现等价证明。AWS s2n-tls、NSA/Galois多项密码库审计。
• Cogent/TrustFoundry (2010s, Data61/NICTA) — 受限函数式语言→C的已证编译器。seL4生态里「提取路线」的真实落地点(只做组件，不做全内核)。
• Certora (2019, Certora Inc.) — 智能合约规范与验证。DeFi工业标准，OpenZeppelin/Compound/Aave常备。
• Event-B/Atelier B/ProB (1990s-2000s) — 精化式开发，铁路信号。巴黎地铁自动化/西门子铁路信号类项目，EN 50128语境下成熟。

三条路线对照

核心差异：提取路线的代价是放弃对底层的控制，精炼路线的代价是写两遍，注解路线的代价是注解负担与重构脆弱性。三者都没有真正「只写一遍」，只是把第二遍的成本转移到了不同位置。

工具归类速查（按 A/B/C 三层）

信任基干净程度排序

从最干净往下：

1. Coq/Isabelle 小内核 + CompCert（可独立检查证明证书）
2. seL4/HOL4 二进制级证明
3. SPARK/Dafny/Verus/F*（Z3 + 运行时假设）—— 求解器版本钉死是硬伤
4. CBMC/Kani/TLA+（有界）
5. Rust 借用检查 + unsafe 审计
6. Astrée/Polyspace（抽象解释，可能误报）
7. 纯认证流程（PikeOS/鸿蒙 EAL 级，流程保证而非定理）

选型建议

按你要证的性质选

三个务实提醒

1. 不要把「起始年份」当成熟度。SPIN 1989、TLA+ 1999 很老但依然主流；Ironclad 很强但已停更。成熟度应由「是否有生产常驻 + 是否有人维护」定义。
2. 强度与成熟度负相关是常态。最强的（Coq/Isabelle 端到端）往往最难落地；最好落地的（Kani/Astrée）给的结论最受限。
3. 留一栏「组合关系」。这些工具极少单独使用，标注互补关系（如 Kani→Verus、TLA++轨迹确认、Astrée+WP）比孤立评分更有用。工业上的实际形态都是组合：TLA+ 管设计 + Verus/SPARK 管 TCB + CBMC/Kani 扫 unsafe + herd7 管内存模型 + CompCert/二进制证明管编译链。

推荐工具

以下推荐基于开源许可、成熟度、活跃度、工业/学术背书四个维度综合筛选，按上手难度从低到高排列。每个推荐都标注了适用场景与不适用场景，方便快速决策。

零注解 / 低门槛路线（先跑起来再说）

适合：想以最低成本获得形式化反馈，团队没有形式化背景。

建议：C/C++项目先用 CBMC 或 ESBMC 跑一轮有界模型检查，零注解成本就能发现不少深层 bug。Rust 项目直接用 Kani。

auto-active 路线（注解负担中等，性价比最高）

适合：团队愿意写少量契约注解，换取自动化验证收益。

建议：

• 新项目选语言时，Rust + Verus 或 Dafny 是性价比最高的组合。
• 已有C代码想补验证，用 Frama-C。
• 已有Java代码想补验证，用 KeY（成熟）或 OpenJML（轻量）。
• 安全关键系统（航空/铁路），用 SPARK。

交互式定理证明器（能力最强，门槛最高）

适合：需要绝对正确性保证的核心组件，团队有形式化专家。

建议：

• 需要验证编译器/核心算法的绝对正确性 → Coq
• 数学/密码学/操作系统 → Isabelle
• 想跟进最新趋势、兼顾编程和证明 → Lean 4

模型检验 / 抽象建模（设计阶段首选）

适合：写代码之前验证设计/协议的结构性质。

建议：在写分布式系统/并发协议之前，先用 TLA+ 或 Alloy 建模验证设计，成本远低于写代码后再改。

按语言生态推荐

如果团队已经锁定某种编程语言，优先选该语言生态内的工具：

综合推荐路径

根据实际项目阶段，推荐以下工具组合路径：

黄金组合推荐

如果只能选几个工具组建团队工具链，以下是经过工业实践检验的"黄金组合"：

核心原则：没有银弹。工业上的实际形态都是组合——TLA+ 管设计 + Verus/SPARK 管 TCB + CBMC/Kani 扫 unsafe + herd7 管内存模型 + CompCert/二进制证明管编译链。根据项目阶段和团队能力，从低门槛工具入手，逐步向上迁移。

最高 ROI 集合小结：

• L1 设计层：
  • 协议、状态机：TLA+, PlusCal, Quint, StateRight(Rust)，TLA+ 最强大但也最难用
  • 模型结构、规则：Alloy，需求分析、设计阶段早发现问题
  • 精化式开发：Event-B
• L2 代码层·自动验证：Miri(Rust，运行时检查), RAPx(Rust，抽象解释，检查 unsafe），Kani(Rust)，ESBMC，Flux(Rust)
• L3 代码层·演绎验证：Verus(Rust), Dafney
• L4 证明助理：Rocq, Lean 4