文章指出，随着AI消除编写证明的成本，形式化验证已进入可广泛使用的阶段，能确保软件业务规则在数学上正确无误，而不仅仅是经过测试。

好的，这是根据您的要求，对原文主要内容进行的中文重述，已保留关键细节并删减了与主题无关的内容。

标题：关于形式化验证，你可能并不了解

核心观点： 形式化验证的成本和工具已发展到可广泛使用的阶段。AI通过消除编写证明的成本，移除了形式化验证最大的障碍。这使得构建具有关键业务规则、且能保证数学上正确（而不仅仅是经过测试）的软件变得前所未有的容易。

问题引入： 如果你的程序有一套复杂的业务规则，你能保证任何有效输入的组合都不会产生无效结果吗？

文章以一个秘密管理平台的权限系统为例。规则控制谁可以读取、编辑或删除不同环境中的秘密。当用户创建自定义角色时，系统会检查新角色的权限是否是用户自身权限的子集（即，你不能授予自己没有的权限）。边界检查覆盖了所有权限操作符的组合，并且通过了全面的测试套件。

但存在一个测试从未尝试过的案例：一个权限仅限单个环境（如QA）的用户，可以创建一个权限为“非开发环境”的角色。“非开发环境”听起来范围很窄，但它匹配除开发环境外的所有环境（如UAT、沙箱、金丝雀、生产等）——这意味着一个单环境权限升级为了近乎通用的访问权限。边界检查批准了它，测试也没有捕获到，因为每个测试都使用了重叠的值。只有当权限集不重叠时，这个bug才会触发。

一个正确设计和实现的权限系统有一个基本的语义不变量：权限派生是子集不变量。即，派生权限匹配的环境集必须始终是授予权限匹配的环境集的子集。这个属性不关心权限如何表示，它涵盖了有限集、否定集以及任何未来可能添加的表示形式。有了这个不变量，权限派生在运行时就不会失败，因为这类bug在构造上就不可能发生。

“代码在运行时没有失败”和“代码不可能失败”之间的区别，正是本文要探讨的。

什么是形式化验证：

其核心概念很简单：从你想要代码遵守的属性开始。这些是输入和输出的契约。例如，对于购物车，你可能想证明： - 余额永远不会为负。 - 购物车中的每件商品都反映在总价中。 - 每个订单只能应用一张优惠券。

这些属性需要用一种“验证感知”的语言来表达。这类语言将规范和证明视为与实现代码同等重要的“一等公民”。例如，Dafny、Lean、Rocq（原Coq）、F*、TLA+等。它们的工作方式不同，但核心思想一致：你在同一个系统中编写代码和属性，工具会检查代码是否满足属性。

以Dafny为例，对于“余额永远不会为负”的属性，你会编写： method ApplyCoupon(balance: int, discount: int) returns (newBalance: int) requires discount >= 0 requires balance >= discount ensures newBalance >= 0 { newBalance := balance - discount; }

requires子句是前置条件，ensures子句是后置条件。验证器不运行代码，而是推理其结构，并将验证条件交给一个自动化的“神谕”（如SMT求解器），以确定后置条件是否对所有满足前置条件的输入都成立。如果成立，证明通过；只要有一个可达状态破坏了属性，代码就无法编译。

这种保证是绝对的：该属性在程序的每个可达状态中都成立。这与测试有本质区别。测试可以采样大量随机输入并捕获一些严重错误，但无法保证覆盖所有情况。验证则告诉你：“这里没有bug可找。”

那么，为什么你以前没用过它？因为历史上，编写证明的成本远超编写代码的成本。工具慢，过程繁琐，需要博士级技能，错误信息难以理解。因此，形式化验证几乎只存在于航空电子、芯片设计、核系统和密码协议等领域——在这些领域，一个bug的代价是生命或巨额财富。对其他人来说，合理的结论是：测试已经足够好了。

现在，形式化验证是AI的问题：

“测试足够”的结论不再成立，因为AI现在可以处理最初阻碍该系统在主流开发中使用的瓶颈。这个瓶颈不是验证本身，而是编写证明：将直观的需求转化为验证器要求的精确逻辑形式，然后在求解器无法自动确认时花费数小时或数天去调整。自Opus 4.5以来，大多数前沿LLM能够根据自然语言需求起草形式化规范，提出证明策略，并且关键的是，能在与验证器的紧密循环中相对快速地迭代失败的引理。

AI提出实现候选方案，一个确定性的、机械化的过程检查每个候选方案的正确性。如果证明错误，验证器会拒绝它，AI会再试一次。对AI的信任被降低（到规范层面），因为验证器是一个外部权威。人类留在需要判断的环节：决定哪些属性值得保证以及进行系统设计。同时，机器处理产生可验证正确实现的工作。

这改变了形式化验证的适用对象。它不再只适用于有预算聘请专业证明工程师的安全关键系统。它适用于任何有值得证明的属性的开发者。

实践中的形式化验证：

考虑一个遵循状态机的电商订单：购物车 → 已下单 → 配送中 → 已送达，已取消可从已下单或配送中到达。需要验证的基本属性是财务守恒：取消时，退款金额必须精确等于未发货商品的价值。等价地，客户支付的净额必须始终等于他们收到的商品价值。

在Dafny中，关键子句是：在已取消状态下，退款金额 == 已收取金额 - 已发货价值。这一行代码为所有可能的取消情况编码了财务守恒定律。每个状态转换都是一个带有前置条件和后置条件的方法，确保每个状态转换都保持有效状态。由此，可以自动推导出财务健康和无资金损失等属性。没有一系列操作——添加商品、下单、发货、取消——能产生一个无效订单。

捕捉意图漂移：

当会计逻辑简单时，财务健康属性在终端状态很容易成立。但后续可能会增加折扣、批量订单等功能。通过预先编码财务守恒属性，你可以确保未来该模型内的任何代码都不能违反这个基本属性。

假设六个月后，产品增加了订单级优惠券。改动看起来很小：在订单上增加一个折扣字段，已收取金额变为商品总价 - 折扣。测试夹具更新了，取消测试仍然通过。但一个bug被引入了：在某些取消场景下，客户被多收费了。

由于订单生命周期是在一个经过验证的域中实现的，折扣功能也必须在该系统内实现。不变量退款金额 == 已收取金额 - 已发货价值在已收取金额 == 商品总价时是正确的。一旦折扣 > 0，已收取金额和商品总价出现偏差，这个不变量就默默地编码了错误的财务定律。验证器不会说语义是否被保留，但它会捕获不变量之间的不一致性。错误本身不会修复bug，但失败表明设计中存在需要解决的差距，以确保之前设定的基本属性（用户不应被多收或少收）不会被违反。因为折扣功能是在一个经过验证的系统中实现的，任何违反不变量的实现都无法编译通过。

证明的好坏取决于规范：

本文所述的一切都假设规范是正确的。这不是一个小假设——这是形式化验证中最难的部分和关键所在。没有工具能完全自动化你希望应用采用的设计决策。验证器会无情地执行你告诉它的任何东西，但它不能告诉你应该执行什么。与AI一起进行头脑风暴和规划，以及在形式化规范编写阶段进行规范冲突审计，有助于设计过程。

回到秘密管理平台的例子，那个bug只有在有人陈述了子集不变量时才能被捕获。如果规范说的是更狭隘的东西，比如“有限权限只能包含其他有限权限”，证明会通过，但保证不会覆盖未来的权限表示形式。不变量需要在正确的抽象级别上陈述，随后的证明也需要在正确的深度上证明它。即使你从未接触过形式化规范或证明，正确做到这两点也需要对领域有深刻的理解。

形式化验证能做什么和不能做什么：

你选择验证的属性，是对系统中什么最重要的一种声明。一旦你把它做对了，保证就是绝对的。

目前，经过形式化验证的核心可以处理大多数无副作用的逻辑——不变量、转换、冲突解决。但UI、网络调用和数据库交互通常位于验证边界之外。验证使核心无懈可击，但不能保证端到端的正确性。

一些工具已经存在，证明的成本现在就是编写它们所需的token成本。有了正确的工具，形式化验证已准备好集成到主流AI工作流程中。

根据评论内容，总结主要观点如下：

1. 形式验证的实用性有限（支持者与质疑者并存）

• 质疑观点：形式验证对大多数应用开发者仍过于局限，尤其对电商等CRUD应用（99%代码涉及I/O）帮助不大。评论1指出：“Formal verification is still too limited to be useful for most app developers... E-commerce apps are mostly CRUD apps; I/O with the database, the UI, and third-party APIs is 99% of the code.” 评论8强调规范本身才是问题：“The spec has always been the problem... The spec has to be just as detailed and will be just as error-prone as the code itself.”

• 支持观点：形式验证在特定领域（如文件解析器）有应用价值，且AI可自动化繁琐部分。评论7认为：“there is enormous potential to use AI to automate the annoying parts of the verification process... many file format parsers are exploitable, but they are simple enough that they could be formally verified.”

2. 成本与可行性问题

• 评论4质疑AI能否降低验证成本：“Whether you pay people to write the proofs or you pay an LLM to write the proof, you still have to pay for it... I see nothing in this article to even suggest why it wouldn't still be 100x more expensive when an LLM is doing the work.”

• 评论9从实践角度指出验证对代码质量的正面影响，但维护成本高：“Proof maintenance as code changes is a pain and I would like LLMs and/or other tools to help with that.”

3. 对文章标题的批评

• 评论3批评文章标题有标题党倾向：“ACM now stooping to the level of clickbait youtubers.”

4. 其他观点

• 评论6质疑形式验证能否处理现实世界的复杂边界情况（如地震、用户去世等），认为模型难以覆盖所有争议状态。
• 评论10和11以幽默方式表达对软件无bug的怀疑：“That there are bugs in it. That would be the only thing I can 100% guarantee.” / “60% of the time it works every time.”

总结：评论者普遍认为形式验证在理论上有价值，但实际应用受限于I/O复杂性、规范编写难度和成本问题。AI可能降低部分验证成本，但能否根本改变现状仍存疑。少数实践者（如评论9）肯定了验证对代码质量的提升，但承认维护成本高。