形式化验证 + 验证向量

确定性不是被测试，而是被证明。

有两种确定性：测试覆盖的确定性，和数学证明的确定性。采样测试只能证明「你恰好写过的那些输入」；受监管行业（金融、保险、政务）的审计问题只有一个：这条规则，对每一个输入都成立吗？

为什么是现在：LLM 有蛮力，但没有方向

LLM 是概率性的——同样的输入，不同的答案。把企业决策交给一个概率分布，审计员终会问：「这个决定，依据是什么？」行业的共识是：让 LLM 理解，让确定性规则引擎决策。但规则引擎的「确定性」通常靠单元测试背书——而测试只能证明你恰好写过的输入。

采样测试回答不了「每个输入都成立吗」，只有证明能。erdl-formal 把 ERDL 表达式内核编译到 SMT（Z3），验证一条规则永不错、永不 fail-open、永不漏拦。

对比

方案	形式语义	开放性
Cedar Analysis	Lean + SMT（AWS 内部使用）	不对外公开，只服务 AWS 自己的策略语言
OPA / Rego	无——「实现即规范」	开源，但语义只由实现定义
erdl-formal	Z3 / SMT，34 节点全覆盖	开源，ERDL 特定语义（金额、时间、决策对象、双向 gloss）

验证向量：跨实现一致性

向量证明「你采样过的那些输入」；形式验证证明「其余的所有输入」。erdl-vectors 是跨实现的验证基准——318 条冻结向量（审计层 78 + 表达式层 240），不属于任何单一实现：任何语言、任何技术栈，都可以只读规范、从零实现 JCS（RFC 8785）+ SHA-256，逐字节重算并比对。

审计层向量：✅ Node.js（参考）· ✅ Go 独立 runner · ✅ Python 独立 runner

240

表达式层向量：✅ Node.js（参考）· ✅ Python 独立 runner

个独立 Runner 落地（Go / Python），仅凭公开规范从零重算

谁、在哪天、通过了多少条向量——是测出来的，不是声称的。

ERDL 确定性自证：三个 Rego 会漂移、ERDL 不会的规则类型

一句话结论

Rego 是一门强大的查询语言，但它的语义模型是「计算满足条件的集合」，不是「做出判定」。当政策条文需要表达「默认拒绝」「全称量词」「语义稳定」这三件事时，Rego 的语义会漂移——而 ERDL 的「判定模型 + 冻结语义」把这三件事做成了内置不变量。

以下三个类型，每条都给出：政策条文 → Rego 的漂移写法 → ERDL 的对应写法 → 可引用的真实证据。

类型 1：默认拒绝（fail-closed）——Rego 把它交给「调用方」，ERDL 把它做进语义

政策条文：「未明确允许的操作，一律拒绝。」

Rego 的漂移：Rego 里 allow / deny 根本不是关键字（OPA 官方 FAQ 原文），fail-open vs fail-closed 是调用方软件的责任。OPA 官方 operations 文档明确写着：

“this logic is entirely the responsibility of the software asking OPA for a policy decision.”

更危险的是，Rego 的「路径缺失」返回 undefined，不是错误（Rego Basics guide 原文：“When a path is missing, the result is undefined, which is not an error!”）。如果调用方忘了处理 undefined，就会 fail-open——放行了本该拒绝的操作。要 fail-closed，必须手写 default allow := false 这种「样板代码」，漏一行就开天窗。

ERDL 的对应：deny-by-default 是求值语义的一部分，不是样板代码。任何求值错误 → DENY（fail-closed），引擎层面保证，不依赖调用方「记得写 default」。

证据：

OPA 官方 Operations 文档（fail-open/fail-closed 是调用方责任）：https://www.openpolicyagent.org/docs/operations
OPA 官方 FAQ（allow/deny 非关键字）：https://www.openpolicyagent.org/docs/faq
Rego Basics guide（undefined 非错误）：https://www.datocms-assets.com/75231/1674577890-rego-guide.pdf

类型 2：全称量词（FOR ALL）——Rego 要「否定 + 存在 + 再否定」，ERDL 有原生 `all`

政策条文：「员工不得将客户数据发送到任何外部域名。」（核心语义：全称量词「任何」）

Rego 的漂移：这条政策是「FOR ALL」，而 Rego 表达 FOR ALL 是反直觉的——必须「补逻辑 + 否定 + 存在 + 再否定」。OPA 官方 policy-language 文档自己承认这是一个「常见错误」：

“A common mistake is to try encoding the policy with a rule named no_bitcoin_miners like so: app.name != "bitcoin-miner" # THIS IS NOT CORRECT.”

即：app.name != "bitcoin-miner" 是「存在一个不等于」，不是「全部不等于」。要正确表达「所有收件人都是内部域名」，得绕成「不存在任何一个外部域名」，再配合 not 的 negation-as-failure 语义——两步否定，极易写反。

ERDL 的对应：原生 all / any / none 量词，语义冻结，直译政策：

# ERDL：DENY 当「存在任何一个外部域名收件人」（any 直译「任何」）
- quantifier:
    kind: any
    over: $.recipients
    predicate:
      compare: { op: ne, left: { field: domain }, right: "internal.example.com" }

政策说「任何」，ERDL 写 any，一字不差；Rego 要「否定 → 存在 → 再否定」，翻两次。

证据：

OPA 官方 Policy Language 文档（FOR ALL 的「常见错误」+ negation-as-failure）：https://openpolicyagent.org/docs/policy-language

类型 3：语义稳定性——Rego 连「格式化」都会改变逻辑，ERDL 语义冻结

政策条文：（任意规则）——这里的「漂移」不在写法，在工具链。

Rego 的漂移：真实 CVE-2022-23628——OPA 的 AST pretty-print（格式化）会重新排序数组字面量，从而改变策略的逻辑：

“pretty-printing an abstract syntax tree (AST) that contains synthetic nodes could change the logic of some statements by reordering array literals.”

也就是说：同一份 Rego 策略，经过一次 opa build -O=1（优化）再格式化，逻辑可能就变了。这是「语义不稳定」的铁证——连格式化这种「应该无副作用」的操作都能漂移语义。

ERDL 的对应：S-expression canonical 序列化（跨实现哈希一致）+ FREEZE-2 冻结（已有节点语义永不改）+ 318 条跨实现验证向量（3 个独立实现逐字节一致）。语义是冻结且被第三方复现验证的，不存在「格式化改变逻辑」的可能。

证据：

CVE-2022-23628（OPA pretty-print 改变逻辑）：https://opencve.alliance.unm.edu/cve?product=open_policy_agent&vendor=openpolicyagent
佐证 CVE-2025-46569（OPA 允许通过 HTTP 请求注入 Rego 代码的 DoS）：https://www.sentinelone.com/vulnerability-database/cve-2025-46569

结论：这不是「ERDL 更好」，是「语义模型不同」

三个类型指向同一个根：

	Rego	ERDL
语义模型	查询（算集合）	判定（allow/deny）
fail-closed	调用方责任（样板代码）	语义内置
全称量词	否定+存在+再否定（易写反）	原生 `all`/`any`/`none`
语义稳定	格式化可改变逻辑（CVE）	冻结 + canonical + 跨实现向量

当治理规则进入「监管举证」场景——需要证明「这个判定是确定的、没被误解、没被工具链篡改」时，Rego 的「查询模型 + 调用方兜底 + 语义可漂移」三件事，恰好是三个风险点；ERDL 的「判定模型 + fail-closed 内置 + 语义冻结」是三个对应的消除点。

这就是 ERDL 的自证：不是比 Rego「功能多」，而是在「规则语义的确定性」这一个维度上，把 Rego 需要靠人肉纪律和运气守住的东西，变成了引擎的数学不变量。

ERDL vs ACS：一个已经在用 AGT 的团队，为什么还需要 ERDL

一、先承认：ACS 已经做对了什么

在谈「为什么还需要 ERDL」之前，先诚实地说清楚 ACS 是什么、以及它已经做得很好的部分——否则这篇文章就没有可信度。

ACS（Agent Control Specification）是微软 Agent Governance Toolkit（AGT）的「无状态、确定性、默认拒绝（fail-closed）的策略决策运行时」。 微软自己的定位是「agent safety 界的 MCP 或 A2A」：MCP 标准化了 agent 怎么连工具，A2A 标准化了 agent 怎么通信，ACS 标准化了 agent 怎么被安全控制。

它定义了三个铁律（spec §1.1）：

铁律	含义
无状态	运行时不留任何影响裁决的可变状态，每次 host 传入完整快照
确定性	相同 manifest + snapshot + mode + dispatcher → 相同裁决
默认拒绝	求值中任何错误 → deny，绝不放行

它把 agent 生命周期切成了 8 个干预点（agent_startup / input / pre_model_call / post_model_call / pre_tool_call / post_tool_call / output / agent_shutdown），每个点产出一个归一化的裁决（allow / warn / deny / escalate / transform）。

ACS 做对的事，我们必须承认：

编排契约——它把「在 agent 生命周期的哪里检查、怎么传输入、怎么执行裁决」这个「脏活」标准化了，还带 Python / Node / .NET / Rust / Go 多语言 SDK。
工程实践的广度——45+ 篇 tutorial 覆盖了沙箱、提示注入检测、MCP 网关、SPIFFE 身份、成本治理、混沌测试……这是一个「已经能开箱用」的工程体系。
生态卡位——「可插拔策略引擎」（Rego / Cedar / custom）让它在任何框架、任何策略语言上都有一席之地。

如果一个团队要的是「给现有 agent 套一层标准的、可移植的策略检查」，ACS 已经够了。 我们不和它抢这个。

二、ACS 的三个「空洞」（它主动放弃的）

但 ACS 有一个结构性特征，是理解「为什么还需要 ERDL」的钥匙：

ACS 是「策略编排契约」，不是「策略语言」。它标准化了「在哪里拦、怎么执行」，却把「规则本身的语义」主动外包给了 Rego / Cedar。

这正是 ACS 的三个空洞：

空洞 1：策略语义没有被「冻结」，也没有被「验证」

ACS 的「确定性」是编排确定性——相同 manifest + snapshot + dispatcher 结果 → 相同 verdict。但「dispatcher」就是策略引擎（Rego / Cedar / custom），它是 host 提供的、可插拔的。

换句话说：ACS 保证「同一个策略引擎跑同一个输入给同一个结果」，但不保证「你写的规则，语义本身是确定的、正确的」。 Rego / Cedar 的求值语义没有被形式化冻结——同一条规则在不同版本、不同实现之间可能存在细微语义差异。ACS 不承诺这块，因为这块本来就不是它的职责。

空洞 2：审计是「事后重建」，不是「决策时密码学固化」

ACS 的审计能力（Decision BOM，Tutorial 50）原文写得非常清楚：

“Reconstructible View……the BOM is reconstructed on demand by querying existing data sources……No new data collection required.”——还有一个 completeness score（0.0–1.0），表示「必需字段被填了多少」。

也就是说：ACS 的审计是事后从日志、遥测、OTel trace 里「重建」决策上下文，而且可能是不完整的（completeness score < 1）。

这和 ERDL 的 Decision Object（DO）是两回事——DO 是决策产生那一刻就用 JCS + SHA-256 密码学固化的，任何独立方用公开规范重算，得到相同的哈希字节。防篡改、防抵赖、可独立重算。

当审计/合规问「凭什么证明这个决策真的是这么算出来的、且没被改过」时，「事后重建」和「决策时固化」是两个不同强度的答案。

空洞 3：委托授权在「代码里」，不在「规范里」

ACS 的委托链（Tutorial 23）做的是「单调范围窄化」（monotonic scope narrowing），子 agent 能力必须是父的严格子集。但它的实现是：

“The SDK enforces this at the API level — delegate() throws an error if the requested capabilities are not a subset.”

窄化规则写在 SDK 的代码里（delegate() 方法里 throws），而不是写在一份「可被形式化验证、可被第三方独立测试」的语义规范里。这意味着：这个安全性质是「微软实现保证的」，不是「数学证明的」。

三、ERDL 补什么，以及怎么组合

三个空洞，正好是 ERDL 的领地：

ACS 的空洞	ERDL 补什么
策略语义未冻结、未验证	语义规范：34 节点表达式树，FREEZE-2 冻结（只增不改），Z3 形式化验证全覆盖
审计是事后重建	决策对象 DO：决策时 JCS + SHA-256 固化，可独立重算，防篡改防抵赖
委托窄化在代码里	委托授权安全模型：5 不变式 + 8 对抗向量，窄化是「可证明、可测试」的语义，不是某家的实现

而且，二者不是二选一，是组合。

ACS 的「custom dispatcher」本来就是为「接入自定义策略引擎」留的口子。一个已经在用 AGT 的团队，可以：

保留 ACS 的全部：8 个干预点、verdict 归一化、多框架 SDK、沙箱/提示注入/身份这些工程实践；
把 ERDL 挂进去：作为那个「custom dispatcher」，让「规则」从「Rego/Cedar 的一段没有形式化保证的逻辑」升级为「语义冻结 + 形式化验证 + 可独立重算决策证据」的 ERDL 表达式。

四、一句话回答

ACS 解决「在哪里拦、怎么执行」，ERDL 解决「规则本身的语义是否确定、能否被独立验证」。

一个已经在用 AGT 的团队，它的「编排」已经被 ACS 覆盖得很好；但它仍然需要 ERDL，当且仅当它开始面对这三个问题：

规则语义要对——不是「这段 Rego 我测过了」，而是「这段规则的语义被形式化冻结、被 Z3 证明过」；
决策证据要硬——不是「事后从日志重建一个可能不完整的 BOM」，而是「决策那一刻就产生可独立重算的密码学证据」；
安全性质要可证——不是「微软的 SDK 这么实现的」，而是「委托窄化是一条可被第三方独立复现、被对抗向量测试的不变式」。

ACS 给 agent 装上了「检查点」；ERDL 给检查点装上了「确定性、可验证的规则语义」。 两者组合，才是一个既能拦、又能证的 AI Agent 治理体系。