erdl-formal

确定性，不是测出来的，是证出来的。

erdl-formal 是 ERDL 表达内核的形式化验证器：把规则编译到 SMT（Z3），做静态性质证明——不是「测试通过」，而是「数学上不存在反例」。

ERDL 是企业 AI Agent 的确定性规则语言（34 节点类型化表达式树 + E1–E12 求值约束）。本仓库回答一个问题：这条规则，在所有输入下，会不会出错、会不会误放行、会不会该拦不拦？

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

LLM 是概率性的：同一个输入，两种回答。把企业决策交给概率分布，审计迟早会问——「这个决定，依据是什么？」

行业共识正在成形：LLM 负责理解，规则负责裁决——在 Agent 前面，必须有一层确定性规则引擎。但规则引擎的「确定性」通常靠单元测试背书，而测试只能证明测过的输入是对的。

金融、保险、政务这类强监管行业，审计只问一个问题：

这条规则，对所有输入都成立吗？

抽样测试回答不了这个问题，回答只能是证明。Cedar Analysis 在 AWS 内部验证了这条路（Lean 形式化 + SMT 符号分析）；erdl-formal 对 ERDL 表达内核做同样的事——把「确定性」从抽样测试升到全量证明。

和 Cedar 同一条路（形式化策略分析），不同的战场：我们证明的是为钱、时间和决策对象而生的企业规则内核。

30 秒，看一个证明

G3 密级访问控制：文件密级 > 操作员密级 → DENY。要证明这条规则可达且 fail-closed：

from erdl_formal.field_contracts import FieldContract, Schema
from erdl_formal.properties import always_denies

schema = Schema()
schema.add(FieldContract(field="file_cls", type="int"))
schema.add(FieldContract(field="op_cls", type="int"))

# when: file_cls > op_cls  →  DENY
rule = ["gt", ["field", "file_cls"], ["field", "op_cls"]]

# 一条断言，同时证明两条性质：
# 1) 可达 —— 字段都在时，密级更高确实触发拦截
# 2) fail-closed —— op_cls 缺失时，比较按 E11 折叠为假，
#    规则绝不产生误放行绕过
assert always_denies(rule, schema, premises=["file_cls", "op_cls"], missing_field="op_cls")

背后没有测试用例，没有抽样。Z3 在所有整数的空间里搜索违反性质的输入：找到，返回可回放的具体反例（能丢回真实引擎复核）；找不到，UNSAT——性质对全量输入成立，证毕。

能证明什么

每个性质都能合成具体反例，反例可回放真实引擎交叉验证——证明 + 差分，双保险。

34/34 节点覆盖，E1–E12 精确语义

• 34 节点全部有 SMT 编码：取值 / 逻辑 / 比较 / 集合 / 字符串 / 存在量纲 / 量词 / 算术 / 时间 / 聚合。
• 关键语义不是「大致对」，是逐位精确：
  • E2 定点小数：scale=14 + half-even——钱，不允许 0.1 + 0.2 式漂移；
  • E8 量词空数组折叠：反空洞真，all([]) 是假不是真；
  • E11 三值逻辑：字段缺失在叶子处折叠为假（非 Kleene，不 fail-open）；
  • E12 tier 折叠、E10 NFC 归一化。

独立验证者：三重独立，逐字节对拍

验证者的可信度来自不看被验证者的答案。erdl-formal 只依据规范（erdl-spec-v2.0）编码，零依赖任何 ERDL 引擎实现，与 erdl（TS 引擎）、erdl-vectors（冻结向量）构成三重独立：

Measurements, not endorsements. 三个独立构建的系统逐字节一致——说明规范足够精确，能支撑独立实现的精确复现。

与 Cedar / OPA 的差异

差异不是「更形式化」——Cedar 的形式化栈是业界标杆。差异在被形式化的东西：ERDL 是为钱、时间、聚合、量词、决策对象与双向自然语言而生的企业规则内核，这些在 Cedar / OPA 的世界里不存在。

架构

ERDL 规则 (S-expression)
   │
   ▼  compiler.py（符号编译器：schema 驱动字段类型 + 量词索引展开）
Z3 TVL 表达式（TVL(τ) = Def | Missing，叶子折叠）
   │
   ▼  properties.py（性质验证）/ resolution.py（裁决参考模型）
sat / unsat + 反例（回放真实引擎交叉验证）

安装

用户（从 PyPI，一条命令）：

pip install erdl-formal

开发者（从源码，可编辑安装，改代码即时生效）：

git clone https://github.com/OpenOBA/erdl-formal.git
cd erdl-formal
python -m pip install -e ".[dev]"   # Python ≥3.11（3.14 开发），z3-solver ≥4.13（5.1.0 验证）

从源码构建分发包（wheel + sdist，供发布 / 离线分发）：

python -m pip install build
python -m build        # 产出 dist/erdl_formal-0.1.0-py3-none-any.whl + .tar.gz

快速上手

pytest                               # 130 全绿
python examples/verify_g3.py         # 验证 G3 密级规则（可达 + fail-closed）
python replay/crosscheck-vectors.py  # 与 erdl-vectors 冻结向量对拍

文档

• docs/semantics.md — 34 节点指称语义
• docs/tvl-encoding.md — 三值逻辑 SMT 编码规范
• docs/field-contracts.md — 验证 schema 契约
• docs/DEVELOPER-GUIDE.md — 二开指南（架构 / 加节点 / 加性质 / API）

贡献与安全

• CONTRIBUTING.md — 贡献流程（先 issue 后 PR / review）
• SECURITY.md — 漏洞私下报，不开公开 issue
• CHANGELOG.md — 变更记录（Keep a Changelog）
• CODE_OF_CONDUCT.md / style_guide.md

许可证

Apache-2.0 · © 2026 深圳市秒镜科技有限公司 (Shenzhen Miaojing Technology Co., Ltd.)