定理证明器与规约语言怎么选:Hillel 一文分清 Lean 与 TLA+

burny_tech · x · 2026-10-30

Hillel Wayne 长文澄清两类形式化工具的区别。Isabelle、Lean、Rocq（原 Coq）是定理证明器，用于证明数学定理和形式化验证，路径有二：把程序翻译进证明器（有翻译出错风险），或用证明器内建语言直接提取可运行二进制。Fizzbee、TLA+、Spin、Alloy、Quint、P 则是规约语言，用于检查程序的高层蓝图，蓝图验证后仍需确认程序与蓝图一致，这是另一个难题。各规约语言侧重不同：P、Spin、Fizzbee 更贴近代码——P 长得像交互状态机，Spin 像 C 加 CSP，Fizzbee 像 Python 方言，代码风格的规约语言更易上手。回应的是「该选 fizzbee/TLA/alloy/Lean/Dafny 等”的选择困难。