50年后，形式化验证真的赢了吗？
The Case Against Formal Verification, 50 Years Later
随着AI编码的兴起，形式化验证正从边缘走向主流，Google Trends搜索量激增，Lean等工具被广泛学习。然而，1979年一篇经典论文曾断言程序验证注定失败，无法提升人们对程序的信心。本文重读这篇50年前的文章，逐一分析其六大论点：从证明的社会属性、规范与实现的脱节，到全自动验证的不可行性，再到现实系统的复杂性。作者指出，虽然全量验证并非万能，但在AI生成代码的时代，精确描述意图和验证正确性变得前所未有的重要。形式化方法不再是魔法棒，而是提升软件可靠性的关键工具之一。
我们坚信程序验证注定失败，无法提升人们对程序的信心。
HN 评论区
113- somat
我常有的一个疑问是："形式化验证凭什么比它要验证的程序更正确？"注意：这里指的不是验证引擎本身的 bug，而是为程序编写的规格说明（spec）。
这倒不是什么大问题，我认为形式化验证是帮助人们逼近正确性的一把利器，但请允许我解释一下我的想法。当编写一个程序时，它的目的是解决某个问题；如果它正确地解决了这个问题，那就没有 bug；如果它错误地解决了这个问题，那些就是 bug。对于复杂问题，事实证明要正确解决它们非常困难（甚至不可能）。那么，为什么会有这种假设，认为形式化验证的规格说明会比程序本身更正确呢？它们都在试图解决非常复杂的问题。
我曾试图通过阅读 sel4 的 git 提交记录来感受一下这个问题，想弄清楚有多少 bug 修复是针对操作系统本身的，又有多少是针对规格说明的。很遗憾，没有得出什么确切的结论，因为他们几乎总是要同时修复两者。在操作系统中发现一个 bug，意味着你的规格说明有问题；而在规格说明中发现一个 bug，则意味着你的操作系统很可能也有 bug。
- ibarrajo
今年我用 Lean 做了很多 "vibe coding"（凭感觉/氛围编程）。
我发现，一旦你确定了那些对你想要保持的保证至关重要的不变量（invariants），整个过程简直令人惊叹。
我自己构建了一个经过形式化验证的工作流引擎，做起来很容易，主要是因为我已经熟知 Cadence 和 Temporal 的陷阱及其基础支柱。
此外，这似乎不是常识，但你其实可以从 Lean 导出编译为 C 的库。有了它们，你既能获得经过验证的高性能代码，又能轻松地在其他地方通过 C 绑定调用它们。
Lean 本身通常没有很好的 IO 栈，但对于小型项目来说已经够用了。
导出库或使用 native_decide 有一个注意事项。一旦导出到 C，ABI 就超出了 Lean 内核的范围，这意味着编译器本身可能会引入 bug。
- mpweiher
反方观点是："规格说明比实现更接近非正式的需求（因此更容易发现错误）。"
我在大学学习形式化验证时，发现的恰恰相反，这也是让我觉得形式化规格说明/验证缺乏吸引力的主要原因。
- gr_norm
如果你没 bothered 去读那篇文章，标题可能会稍微有点误导性。这篇文章是在回应一篇 1979 年批评形式化验证的著名论文。文章最终在回顾时不同意该论文的大部分最强有力的观点，尽管其中一两点似乎仍然有价值。
- sp1982
假设我用 Rust 写了一个分布式算法。为了验证它，我可能会用 TLA+ 重新描述该算法，对该规格说明进行模型检测，并证明它满足我关心的属性。
现在我有两个产物：
TLA+ 规格说明 --> 已证明
Rust 实现 --> 运行时
但证明建立的是类似这样的关系：
TLA_Spec => Safety
而我真正需要的是：
Rust_Program => Safety
我相信这被称为 "模型 - 代码差距"（model-code gap），虽然有方法可以解决它，但我还没找到一种易于遵循的方法。