erdl-formal

🚀 POC welcome — we encourage you to try this project as a proof of concept in your own environment. For technical support, contact us anytime at support@openoba.com.

A formal verifier for the ERDL expression kernel — proving rule safety over all inputs with Z3.

There are two kinds of determinism: the determinism tests cover, and the determinism mathematics proves. erdl-formal provides the latter.

"erdl-formal formally verifies ERDL v2.1's expression kernel and evaluation semantics (§5, §7, Appendix A), covering all 34 nodes and the evaluation-semantics constraints E2/E8/E10/E11/E12 (plus E3 division-by-zero). The engine-layer constraints E1 (purity), E4 (resource limits), E5 (when/expr exclusivity), E6 (tree hashing), E7 (single evaluator), and E9 (no wall clock) are runtime/compile-layer concerns, not kernel evaluation semantics — the spec's other layers (document structure, gloss rendering, integration modes) are guaranteed by test vectors and engineering verification."

Why now: LLMs have brute force. They don't have direction.

LLMs are probabilistic: same input, different answers. Hand enterprise decisions to a probability distribution, and the auditors will eventually ask — "on what basis was this decision made?"

The industry is converging on an answer: let the LLM understand; let a deterministic rule engine decide. But a rule engine's "determinism" is usually underwritten by unit tests — and tests only prove the inputs you happened to write.

In regulated industries — finance, insurance, government — the audit question is singular:

Does this rule hold for every input?

Sampled tests can't answer that. Only a proof can. Cedar Analysis proved this approach works inside AWS (Lean formalization + SMT symbolic analysis). erdl-formal does the same for the ERDL expression kernel — lifting determinism from sampled testing to exhaustive proof.

• Cedar Analysis: used inside AWS, Lean + SMT, not open to the public, serving only AWS's own policy language.
• OPA/Rego: no formal semantics — "the implementation is the spec."
• erdl-formal: open source, 34-node full coverage, ERDL-specific semantics (money, time, decision objects, bidirectional gloss).

One proof in 30 seconds

The G3 classification gate: file classification > operator classification → DENY. We want to prove the rule is both reachable and fail-closed (a missing field never opens a bypass):

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"]]

# One assertion, two properties at once:
# 1) reachable — with both fields present, a higher classification fires the block
# 2) fail-closed — a missing field never opens a bypass. This depends on the
#    document's unmatched fallback (default_decision): under a DENY fallback the
#    silenced guard still denies; under the ALLOW fallback (resolution default)
#    the missing field falls through to ALLOW — the rule fails open.
assert always_denies(
    rule, schema,
    premises=["file_cls", "op_cls"],
    missing_field="op_cls",
    default_decision="DENY",
)
assert not always_denies(
    rule, schema,
    premises=["file_cls", "op_cls"],
    missing_field="op_cls",
    default_decision="ALLOW",
)

No test cases. No sampling. Z3 searches the space of all integers for an input violating the property: if one exists, you get a concrete, replayable counterexample (re-checkable against the real engine); if not, UNSAT — the property holds for every input. QED.

What you can prove

Expression-layer properties (always_denies / subsumes / …) are proven by writing the negation as constraints and checking UNSAT; the ERDL-specific resolution properties (override_soundness / ring_respect / emergency_shortcut / workflow_shortcut / catch_all_inert_when_explicit / catch_all_then_irrelevant_when_explicit / catch_all_override_irrelevant_when_explicit) are encoded in resolution_smt.py, which compiles resolve()'s ring / override / priority ordering into Z3 constraints and proves them UNSAT over every rule-set of exactly n modeled positions (a bounded exhaustive proof at cardinalities n∈{2,3,4}, not sampling — but also not an unbounded proof over arbitrary length). Any SAT counterexample is a concrete rule-set replayed against the real engine — proof plus differential testing, double insurance.

34/34 nodes, E2/E8/E10/E11/E12 evaluation semantics

• All 34 nodes have SMT encodings: value / logic / comparison / set / string / existence / quantifier / arithmetic / time / aggregate (comparison and existence dispatch by field type: int / string / bool; epoch_ms supports date-only and ISO 8601 datetime with time / offset).
• The hard semantics aren't "roughly right" — they are bit-exact:
  • E2 fixed-point decimals: scale=14 + half-even — money is not allowed 0.1 + 0.2 drift;
  • E8 quantifier empty-array folding: anti-vacuous-truth — all([]) is false, not true;
  • E11 three-valued logic: missing fields collapse to false at the leaves (not Kleene); whether a missing field fails open is resolved by the document fallback (see always_denies's default_decision);
  • E10 NFC normalization; E12 evaluation errors collapse to Missing (tier≤2 fail-close is runtime behavior, not modeled in the kernel).

Independent verifier: three-way, byte-for-byte

A verifier is only credible if it never peeks at the examinee's answers. erdl-formal encodes the spec alone (erdl-language-spec), with zero dependency on any ERDL engine implementation, forming a three-way independent cross-check with erdl (the TS engine) and erdl-vectors (frozen vectors):

Measurements, not endorsements. Three independently built systems agreeing byte-for-byte means the spec is precise enough to sustain exact independent reimplementation.

How it differs from Cedar / OPA

The difference is not "more formal" — Cedar's stack is the benchmark, and we say so. The difference is what gets formalized: ERDL is an enterprise rule kernel built for money, time, aggregation, quantifiers, decision objects, and two-way natural language — none of which exist in the Cedar / OPA world (the — rows above).

Architecture

ERDL rule (S-expression)
   │
   ▼  compiler.py (symbolic compiler: schema-driven field typing + quantifier index unfolding)
Z3 TVL expressions (TVL(τ) = Def | Missing, leaf collapse)
   │
   ▼  properties.py (property checks) / resolution.py (resolution reference model)
sat / unsat + counterexample (replayed against the real engine)

Installation

Users (from PyPI, one command):

pip install erdl-formal

Developers (from source, editable install, changes take effect immediately):

git clone https://github.com/OpenOBA/erdl-formal.git
cd erdl-formal
python -m pip install -e ".[dev]"   # Python ≥3.11 (developed on 3.14), z3-solver ≥4.13 (verified on 5.1.0)

Build a distribution (wheel + sdist, for release / offline distribution):

python -m pip install build
python -m build        # produces dist/erdl_formal-<version>-py3-none-any.whl + .tar.gz

Quick start

pytest                               # all passing
python examples/verify_g3.py         # prove the G3 classification rule (reachable + fail-closed)
python replay/crosscheck-vectors.py  # cross-check against erdl-vectors frozen vectors

Documentation

• docs/semantics.en.md — denotational semantics for all 34 nodes
• docs/tvl-encoding.en.md — three-valued logic SMT encoding
• docs/field-contracts.en.md — verification schema contracts
• docs/DEVELOPER-GUIDE.en.md — developer guide (architecture / adding nodes / properties / API / build & publish)

Acknowledgments

The resolution-layer properties (override_soundness / ring_respect / emergency_shortcut / catch_all_inert_when_explicit) were shaped in part by external review. In particular, ANP2 Network (dev.to/anp2network) provided two rounds of precise, reproducible review of the resolution semantics, across three concrete findings, each identifying a boundary in the kernel:

• string/bool eq/ne/exists (v0.1.2) — the kernel only compiled int equality/existence, raising Sort mismatch on string equality;
• always_denies fail-closure direction (v0.1.2) — the property proved silence rather than fail-closure, backwards under an ALLOW fallback;
• the catch-all relax-direction gap (v0.1.17) — a catch-all (empty- condition) ALLOW could rewrite an explicit DENY across rings, and the relax direction had no property watching it.

Each finding moved from a spec/engine/property gap to a fix, a test, and a proof. The project is sharper for it.

RavindraAnnam (github.com/RavindraAnnam) reviewed resolution_smt.py and test_resolution_smt.py against the SPEC §7.1 text, and sharpened the assurance boundary: the resolution properties are proven UNSAT at each checked cardinality (n ∈ {2,3,4}), not over arbitrary rule-set length, and the wording now states exactly that — a bounded exhaustive proof rather than an unbounded claim. That precision is what makes the assurance boundary independently auditable.

A follow-up pushed that boundary one step further with small-model evidence (not proof): the harness also holds UNSAT at n=5 and n=6, and every gate-mutant counterexample at n=6 greedily shrinks to 2 rules — evidence that the interesting witnesses live at cardinality ≤2, inside the exhaustively-checked region. The named open item is the induction that would turn the "≤2-rule witness" claim into a genuine small-model theorem; until then the assurance remains bounded. Reproducible under replay/small-model-experiment.py, replay/witness-shrink.py, and replay/independence.py.

Contributing & security

• CONTRIBUTING.md — contribution process (issue-first, review)
• SECURITY.md — report vulnerabilities privately, no public issue
• CHANGELOG.md — changelog (Keep a Changelog)
• CODE_OF_CONDUCT.md / style_guide.md

License

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