Metadata-Version: 2.4
Name: erdl-formal
Version: 0.1.19
Summary: SMT-based (Z3) formal verification for the ERDL expression kernel — proving rules safe over all inputs.
Author-email: OpenOBA <support@openoba.com>
License: Apache-2.0
Keywords: erdl,formal-verification,smt,z3,cvc5,policy,ai-agent,deterministic
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE
License-File: NOTICE
Requires-Dist: z3-solver>=4.13
Provides-Extra: dev
Requires-Dist: pytest>=8; extra == "dev"
Dynamic: license-file

# erdl-formal

[![Version](https://img.shields.io/badge/version-v0.1.19-blue)](https://github.com/OpenOBA/erdl-formal/releases) [![License](https://img.shields.io/badge/license-Apache%202.0-green)](LICENSE) [![SMT](https://img.shields.io/badge/verification-SMT_Z3-0082c8)]() [![Kernel](https://img.shields.io/badge/kernel-34_nodes-blueviolet)]() [![Coverage](https://img.shields.io/badge/coverage-34%2F34_nodes-green)]() [![Python](https://img.shields.io/badge/python-3.10%2B-3776AB)]()

> 🚀 **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](mailto: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):

```python
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

| Property | Meaning | Origin |
|---|---|---|
| always-denies | fires whenever its guard can — whether a missing field opens a bypass is resolved against `default_decision` | Cedar + E11 |
| subsumption / equivalence / disjointness | implication / equivalence / mutual exclusion | Cedar |
| override-soundness | overrides go DENY→ALLOW only (never toward a less-safe state) | **ERDL-specific** |
| ring-respect | a higher-ring DENY overrides a lower-ring ALLOW (ring order honored in the DENY direction) | **ERDL-specific** |
| emergency-shortcut | EMERGENCY_HALT short-circuits the moment it fires | **ERDL-specific** |
| catch-all-neutral | a catch-all (empty-condition) rule never rewrites an established decision, in either direction (EMERGENCY_HALT excepted) | **ERDL-specific** |

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` / `catch_all_neutral`) are encoded in `resolution_smt.py`, which compiles `resolve()`'s ring / override / priority ordering into Z3 constraints and proves them UNSAT over **all rule-sets** — not sampling, a full proof. 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`](https://github.com/OpenOBA/erdl-landing/blob/main/erdl-spec.en.md)), with zero dependency on any ERDL engine implementation, forming a three-way independent cross-check with [`erdl`](https://www.npmjs.com/package/@openoba/erdl) (the TS engine) and [`erdl-vectors`](https://github.com/OpenOBA/erdl-vectors) (frozen vectors):

| Cross-check | Pair | Result |
|---|---|---|
| Fixed-point | `fixed_point.py` ↔ erdl `fixed-point.js` | byte-identical |
| Resolution | `resolution.py` ↔ `resolution_smt.py` (Z3 model; semantics aligned to erdl-landing `evaluator.ts`) | exhaustive + random differential (`test_resolution_smt.py`) |
| Arithmetic vectors | ↔ erdl-vectors V-ENGINE | 7/7 |
| Calendar vectors | ↔ erdl-vectors V-ENGINE | 6/6 |
| G3 counterexample replay | `tvl.py` ↔ erdl engine | scenario-identical |

**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

| Dimension | Cedar Analysis | OPA / Rego | **erdl-formal** |
|---|---|---|---|
| Formal verification | ✅ Lean + SMT (the field's benchmark, closed) | ❌ no formal semantics — the implementation *is* the spec | ✅ SMT (Z3), open source |
| Fixed-point (money) | decimals only via extension plugin | float64 loses precision | ✅ scale=14 + half-even |
| Time / calendar | — | — | ✅ UTC calendar (days_between / date_add / date_part / month-end) |
| Aggregation | — | — | ✅ aggregate (count / sum / avg / min / max) |
| Quantifiers | — | — | ✅ all / any / none (E8 empty-array fold) |
| Decision object | policy IDs only | unsigned logs | ✅ rich DO + hash chain |
| Natural language | one-way (NL→policy) | one-way | ✅ deterministic gloss, anchored round-trip (two-way) |

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):

```bash
pip install erdl-formal
```

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

```bash
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):

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

## Quick start

```bash
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_neutral`) were shaped in part by external
review. In particular, **ANP2 Network** ([dev.to/anp2network](https://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.

## 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.)
