要点
- 形式化策略在重排或换成等价谓词之后，文本 diff 看起来会像两份完全不同的文件；而真正的含义变化，例如需求写的是并且、译文写成或者，却可能被噪声盖住。
- 该引擎计算两个表达式的最具体公共模式，也就是 Plotkin 在 1970 年提出的反合一，并在记录了代数定律和领域规则所推出等式的 e-graph 上进行。
- 在那个策略例子里，统一 diff 把 28 行中的 18 行标成改动。在按结合律和交换律规范化，并加入关于获批区域的领域改写之后，剩下的分歧是 And 变成了 Or，以及 Lte 变成了 Lt。
- 代码以 Apache-2.0 发布在 github.com/yaspar-org/semi-persistent。在该例子上，默认搜索的 3000 次随机试验复现了精确求解器的最优结果。
- 用 Verus 验证的容器层报告，快照恢复有 1703 条已验证条件、0 个错误。完整求解器还没有端到端的精化证明，记录下来的理由也还不是可被独立回放检查的证书。
2026年11月11日，AWS AI Labs 发表了一种按含义、而不是按文本比较形式化策略的方法。眼下最直接的用途是自动形式化：用语言模型把需求文档写成形式化文本。再跑一次，可能得到另一份形式化结果，旁边并没有标准答案。模型负责写出那份文本，并不参与计算 diff。审查要解决的问题是：两个候选在哪里一致，又在行为上分开。
[1][2]语义策略 diff 如何工作
语义 diff 要显示两份策略的共同点，以及它们在哪里不一致。引擎寻找两个表达式的最具体公共模式。这就是 Plotkin 在 1970 年给出的反合一经典表述。它运行在 e-graph 上，这种结构会保存一个项，以及目前已知与它相等的所有项。团队提供代数定律和领域规则，例如把“外部目的地”和“不是内部目的地”视为相等。共同结构只打印一次。每一处真正的分歧保留为带两种读法的 Variants 节点。若没有剩余差异，则在这些定律和规则之下，两份策略等价。若规则或搜索不完备，剩下的差异也可能只是引擎尚未发现的等价。这个限制写在原文里，每次使用都应当一并记住。
实现上的选择很具体。结合律、交换律和幂等律是数据结构的性质，而不是会把等价副本灌进图中的改写规则。精确的动态规划求解器可以在“先求更小结果”的目标以及当前图的条件下找到最优解。默认算法则是可随时给出当前最好答案的蒙特卡洛图搜索。半持久化快照让引擎可以比较许多候选，而不必每次都复制整张图。
面向的目标包括 SMT-LIB，也就是 Z3 这类求解器的标准输入，以及 Cedar 和 Dogwood 授权策略、规定智能体文件系统和网络访问的 OpenShell 沙箱规则，还有嵌在应用里的 CEL 表达式。
[1][2]一个可逐步核对的例子，不是打分语料
最清楚的证据是一个小而可核对的例子，不是大型基准。两份策略编码在文本上有五处不同。三处是表面的：合取项重排、相等比较的参数对调，以及把 approvedRegion 谓词展开成 us-east-1 和 eu-west-1。两处改了算子：在机密对象条款里 And 变成了 Or，在大小阈值上 Lte 变成了 Lt。统一文本 diff 把 28 行中的 18 行标成改动，并且不说明这五处里哪些真正改变了含义。
语义 diff 去掉了重排和对调后的相等比较，因为在已声明的定律下它们是等价的。加入一条领域改写、说明获批区域恰好就是这两个之后，关于区域的差异也消失了。剩下的是机密条款：第二份编码接受“同一账户”或“加密”两者之一，因而允许机密对象的跨账户复制；以及大小阈值的严格程度。这正是人在审查时真正需要看到的东西。
博文还走查了 Cedar、Dogwood、OpenShell 和 CEL 的例子，包括“必须同时满足所有权和批准”对“满足其一即可”，以及智能体网络访问范围上的分歧。这些是同一比较方法的示意，并不是带标签、已打分的策略对集合。
[1][2]验证了什么，尚未验证什么
仓库是公开的，博文要求读者构建来自第 103 号拉取请求的固定修订。在上述例子上，默认搜索的 3000 次随机试验复现了精确最优解。e-graph 的容器层用面向 Rust 的验证器 Verus 做过验证。所声称的性质是：恢复操作能再现对应快照压栈时的状态，共 1703 条已验证条件、0 个错误。反合一的代码库证明了目标顺序和下界引理，但还没有证明完整求解器符合其规格。引擎可以为推出的每一个等价记录理由。这些记录目前还不是可被独立回放检查的证书。作者把主张清单放在仓库里。对可能用在授权策略上的工具来说，这条限制应当写进任何介绍文字。
[1][2]一个公平的反对意见
这种方法不能告诉你，哪一份形式化文本符合原来的散文，或符合现实世界。它只告诉你，在你声明自己相信的那些等式之后，两份形式化文本在哪里不同。若你漏写一条领域事实，无害的用词差异会看起来像缺陷。若规则过强，真正的分歧也可能被改写掉。目前没有在带已知标签的大规模策略对上报告精确率或召回率。原文称，在对结合和交换算子做了原生规范化之后，亚秒级查询已可实用，但并没有按策略规模公布时间表。持怀疑态度的编辑应当把这些例子看作存在性证明，等到有带标签的评估，再把它当成标准审查关卡。
[1][2]未来六个月该看什么
有用的检验是：自动形式化流水线会不会开始用这个引擎或类似工具，把等价候选归并到一起，只把反复出现的分歧交给人或求解器。值得关注的是，会不会出现针对 Cedar 策略或智能体沙箱规则的公开评估，并统计有多少等价改写被正确忽略、有多少含义变化被正确保留。若这样的评估没有出现，这个工具就仍是一个做得很认真的实验室示例。若出现了，把两份模型输出贴进文本 diff 就会显得不够用，就像凭肉眼比较两份 3000 行的文件，而这正是原文开头的比喻。
[1][2]