形式验证的反对之声：50年后

# 《形式化验证之辩，五十年后》 来源：https://ivan-gavran.github.io/0-social-processes-paper 工程师们对软件验证的热情正在高涨！这或许令人意外，因为长期以来，验证仅在极少数领域有用（乐观而言）；更悲观的看法则认为其不切实际、毫无用处，甚至纯属时间浪费。然而，围绕它的热潮已然显现：过去两年“形式化验证/形式化方法”的搜索量在谷歌趋势上急剧攀升，人人都在学习Lean语言，新的规约语言层出不穷，甚至出现了端到端验证重大应用的尝试（例如Signal Shot项目：https://www.beneficialaifoundation.org/blog/signal-shot）。 这股热情的主要推动力是AI编程。首先，AI智能体在其编写的程序中留下了理解空白，因此催生了对其他正确性保障手段的需求。其次，验证本身也变得更快捷，更容易融入现实世界的软件开发流程。第三，对商业而言（或许也是最重要的），如果编写程序变得极其迅捷，未来的所有收益都将聚焦于软件正确性保障领域。 Antithesis公司的Will Wilson在其题为《我们赢了，然后呢？》的演讲（https://youtu.be/9O6T-iyC4yA?si=QAWBZFlmyeFs9_XM）中宣告了这个传统小众领域的胜利（该演讲作为Bug Bash 2026的开场非常精彩，它为验证社区的未来发展提供了诸多思路，尤其考虑到其正被主流接纳）。 在这胜利的背景下，重读一篇反对形式化验证的经典论文《社会过程与定理及程序的证明》（https://dl.acm.org/doi/10.1145/359104.359106）饶有趣味。1979年，其作者写道： *“我们认为（……）程序验证注定会失败。我们无法想象它如何能提升任何人对程序的信心。”* 我将梳理论文中的论点，并探讨近期发展（如果存在）是否已推翻它们。这是一项有趣的尝试，而非完全严肃的审视：论文实际上并非断言所有形式化方法都将失败（仅针对完全验证而言）。此外，验证是否会成为软件工程常规组成部分仍不明朗（目前所见仅是兴趣萌芽）。尽管如此，在2026年重新审视五十年前被视为根本性的障碍，或许仍具启发意义。 ## 论点一：验证的沟通价值存疑 作者指出，程序证明无法与数学证明类比。他们认为：编程不应像数学那样，将每个程序视为需要证明的定理。因为即便在数学中，定理证明也非终点，而是沟通的起点。真正的关键在于其他数学家内化该证明，并将其与其他数学分支或现实世界建立联系。整个过程共同构建了命题的可信度。 这一点无可反驳：程序证明无需与数学完全对应（该论点针对特定动机，而非软件验证的基础）。 ## 论点二：规约本身的问题 第一部分论证如下：现实世界存在非形式化的需求（相关方对其有共同的直觉理解）。这种直觉性的非形式化需求需转换为形式化规约，而该转换过程本身是非形式化的。在此未经验证的过程中，大量信息可能丢失或被误解。 这观点很合理。但反驳在于：规约比实现更贴近非形式化需求（因此错误更易发现）。此外，现代规约语言（如Quint：https://quint.sh/）支持交互式检查规约及其所有边缘情况，确保其真正契合我们的直觉。 第二部分论证指出，规约的价值仅在于其独立于实现。鉴于软件开发的迭代特性，这几乎不可能实现。一旦失去独立性，我们实际上只是在对齐规约与实现（并可能向两者引入相似错误）。 我认为即使在过去这也不是强有力的论点，尤其当编程智能体介入时。每当获得额外理解，这对开发过程整体都是有益的。人类作为最终仲裁者，决定如何调整规约并重新审视初始假设。编程智能体可被允许生成、修改代码及生成证明。但若需修改规约，仅有人类能以“正确”含义的最终定义者身份执行——这便将我们带回论点二的第一部分。 ## 论点三：全自动验证遥不可及 在论述验证作为沟通手段的缺陷后，作者转向全自动验证器的潜力（此时即便证明未引发同行间的社会过程，我们仍可因程序被证明正确而满足）。作者认为全自动验证器极不可能实现。 此后，自动验证器开发取得一定进展，但人类工作（编写证明或编写适用于模型检测的模型）仍至关重要。然而，大语言模型驱动的工具正快速弥合这一差距。Igor Konnov在其文章《AI为分布式协议提供形式化证明可能比你想象的更近》（https://protocols-made-fun.com/proofs-are-closer.html）中描述了在Lean中证明Ben-Or协议安全性的经历。 ## 论点四：即使全自动验证可实现，也将有害 作者声称，仅回应“已验证”或“未验证”的验证器无助于理解，会让程序员对后续修改束手无策。此外，他们认为，已验证的程序可能会降低对其他防御层（如监控、速率限制等）的重视。 这是个薄弱论点，基于对自动验证存在下验证工具及程序员行为的最坏假设。 ## 论点五：现实系统过于复杂无法规约 文章正确指出算法与现实系统存在巨大差异。算法规约往往简洁整洁，而现实系统的规约则是临时性、不稳定且杂乱的。此外，大多数现实系统中算法简单易懂（因此验证它们价值不大）。 确实，并非所有系统都需要验证。但近几十年来，以下变化推动了对更多验证的需求： - 软件进入关键基础设施和金融领域，风险加剧。 - 若希望编程智能体创造出符合预期的成果，我们最好能清晰描述需求。当然，这不一定需要形式化规约，但与编程智能体合作时，精确规约意图的目标愈发重要（这不意味着完全验证，但规约艺术本身也是形式化方法工具之一）。 ## 论点六：软件可靠性远不止验证 *“使程序正确的愿望是建设性且有价值的。但整体化的验证观，忽略了接受类似于真实数学证明的正确性标准或真实工程结构可靠性标准可能带来的益处。在经济限制内追求可行性、通过复用成功设计引导创新的意愿、对同行群体运作的信任——所有使工程和数学真正运作的机制，在对完美可验证性的徒劳追求中被掩盖了。”* 我完全认同此观点。确实，系统的完全验证很少是提升可靠性的最佳途径。所有其他迈向软件正确的努力同样重要。二者并非竞争关系：关键在于更关注实现正确性的最佳方法。 ## 结论 这是一篇读来颇有趣的论文。作者提出了一个重要观点：形式化验证并非解决所有正确性问题的魔杖。正如他们指出的，软件正确性涉及远不止验证：工程流程、商业考量、额外防御层等等。 由于聚焦于完全验证，论文作者错误地否定了形式化方法各组成部分对整体理解、更优设计选择或更高速度的价值。当AI编程智能体编写代码时，所有这些都被放大，人类则承担起规约编写内容并检查是否按给定规约实现的任务。这也使编程智能体的工作更便捷：验证为其提供了闭环反馈，以判断所写内容是否正确。 --- 感谢两位形式化方法从业者Thomas Pani（https://thpani.net/）和Ranadeep Biswas（https://ranadeep.in/）就论文及本文进行的有益讨论。同样期待听到圈外人对形式化方法依然无用的看法。