Proving Your AI Agent Rules Hold for Every Input — Not Just the Ones You Tested

Here's a question your auditors will eventually ask: "This decision the agent made — on what basis?"

LLMs are probabilistic. Ask twice, get two answers. If your enterprise delegates approvals, refunds, or access decisions to an agent and the only thing standing between it and a bad call is a prompt, you don't have governance — you have a probability distribution with a job title.

The industry is converging on an answer: the LLM handles understanding; rules handle the verdict. Put a deterministic rule engine in front of the model, and let it decide what the agent may and may not do, no matter what the model says.

But here's the uncomfortable part: how do you know the rules themselves are deterministic?

Most rule engines back that claim with unit tests. And unit tests prove exactly one thing: the inputs you tested behave correctly. They say nothing about the inputs you didn't test.

This post is about closing that gap — with three open-source projects that attack the problem at three different levels:

Together they move "deterministic" from a claim to a measurement — and, in the limit, to a proof.

Layer 1 — ERDL: a language where "deterministic" is the point

ERDL (Entity-Rule Definition Language) is a declarative rule format for AI agent behavior governance. The core idea is a when → then decision expressed in plain YAML:

protocol: "erdl/v2"
version: "2.1.0"
metadata:
  name: "refund-guard"
  decision: ALLOW
rules:
  - name: "SEC-001-refund-limit"
    priority: 10
    when:
      logic: AND
      conditions:
        - field: "tool.name"
          operator: eq
          value: "issue_refund"
        - field: "tool.args.amount"
          operator: gt
          value: 5000
    then: REQUEST_HUMAN
    message: "Refund amount over 5000, human approval required"

Three things make this different from "just YAML config":

1. A single semantic tree. Every rule compiles to one of a 34-node expression tree — the same tree whether you wrote it in the Simple projection (30 operators), the Expression projection, or a decision table. Three ways to author; one way to mean.

2. A precise evaluation semantics. The tree is evaluated under a set of named constraints (E1–E12) that pin down the fuzzy parts of real-world rules: fixed-point decimal arithmetic for money (scale=14, half-even rounding — so 0.1 + 0.2 can't drift), three-valued logic for missing fields (a missing field folds to false, so nothing fail-opens), empty-quantifier folding (all([]) is false), and NFC string normalization.

3. Auditable by construction. Every evaluation produces a hashable, chainable Decision Object — the audit record of which rule fired, on what input, with what context.

The reference implementation ships as an npm package:

import { loadErdlFile, Evaluator } from '@openoba/erdl'

const { rules, metadata } = loadErdlFile('refund.erdl.yaml')
const result = new Evaluator().evaluate(rules, {
  tool: { name: 'issue_refund', args: { amount: 8000 } },
  'metadata.decision': metadata.decision,
})
console.log(result.decision) // 'REQUEST_HUMAN'

But a language is only as trustworthy as the claim "every implementation of it agrees." That's where the second layer comes in.

Layer 2 — erdl-vectors: trust is measured, not endorsed

erdl-vectors is a cross-implementation verification benchmark: 301 frozen test vectors that don't belong to any single implementation.

The mechanism is deliberately adversarial to hand-waving:

• A neutral spec. Vectors are generated from the spec alone, with answers stored in a physically isolated file (.gitignored) so nobody can "pass" by reading the oracle.
• First-principles verification. A runner must re-implement JCS (RFC 8785) and SHA-256 from scratch — no json-canonicalize, no SDK — then recompute every Decision Object hash byte-for-byte.
• A canary for honesty. One vector (K01) is generated by a deliberately broken implementation. A correct runner must report it as a mismatch. A runner that skips independent recomputation and just echoes the expected answer gets caught on the spot.

The audit layer (78 vectors) is now verified byte-for-byte by two independent third-party runners — one in Go (norviq-go), one in Python (concordia-python, by Erik Newton of Concordia) — each matching 107/107 canonical bytes.

The principle behind all of this is captured in the repo's own line: "Neutrality isn't declared — it's measured." The registry records who, on what date, passed how many vectors — nothing more. Nobody gets an endorsement; the numbers speak for themselves.

This matters because it answers the question "is the spec right, or does the reference implementation just agree with its own generator?" Only when multiple unrelated implementations, built from the spec text alone, converge byte-for-byte do you have evidence that the standard itself is sound.

Layer 3 — erdl-formal: from "tested" to "proven"

Here's the thing about test vectors, even 301 of them: they are samples. Vectors prove the cases you chose to include. They can never prove the cases you didn't.

erdl-formal is the layer that closes that gap. It compiles ERDL's expression kernel into SMT (via Z3) and proves properties over all inputs — not a sample, the entire space.

A single assertion proves two things at once:

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

assert always_denies(rule, schema,
                     premises=["file_cls", "op_cls"],
                     missing_field="op_cls")

Behind that one line, Z3 searches the space of all integers for a violating input. If it finds one, you get a concrete counterexample you can replay against the real engine. If it finds none — UNSAT — the property holds for every input, and the proof is complete.

What can it prove?

• never-errors — evaluation never throws
• always-denies — hit means block (including fail-closed: a missing field can't bypass the rule)
• always-allows / subsumption / equivalence / disjointness
• override-soundness — an override can only relax DENY→ALLOW, never tighten toward a less safe state
• ring-respect and emergency-shortcut — ERDL-specific semantics that Cedar/OPA don't even model

The three "ERDL-specific" properties are the interesting ones: they're not generic policy properties, they're guarantees about this language's money, time, aggregation, quantifier, and decision-object semantics — the parts that make ERDL an enterprise rules kernel rather than a generic policy DSL.

A note on scope, because honesty builds trust: erdl-formal proves the expression kernel — the full 34-node tree and the E1–E12 constraints. Document structure, gloss rendering, and integration patterns are covered by the vectors and by engineering verification, not by SMT. It's a precise claim, and the precision is what makes it worth something.

Why all three — and not just the proof?

Because they answer different questions, and each one makes the next credible:

• ERDL gives the language a canonical meaning — without it, there's nothing to prove about.
• erdl-vectors proves that meaning is reproducible — that independent implementations, from the spec alone, converge byte-for-byte.
• erdl-formal proves that meaning is safe — that the semantics hold over all inputs, not just the sampled ones.

A language without vectors is "trust my implementation." Vectors without a language are just a benchmark for something no one uses. Proof without vectors is a proof of a semantics only you implemented — which is a proof about your code, not the standard.

Layered together, they're the difference between "our rules engine is deterministic" (a claim) and "here is the language, here is the byte-for-byte agreement, here is the proof" (an audit trail).

Why this matters now: A2A is coming

The urgency isn't just about single agents. As agent-to-agent (A2A) protocols grow, agents will start delegating decisions to each other — one agent approves, another acts, a third records. In that world, cross-implementation trust can't rest on bilateral agreements between vendors. It has to rest on something any independent party can verify.

That's the standardization path this stack is built for: three independent implementations, one open spec, no single owner. Every new independent runner is a brick in the trust infrastructure for the agent economy.

Try it

• ERDL engine — npm install @openoba/erdl · spec · MIT
• erdl-formal — pip install erdl-formal · repo · Apache-2.0
• erdl-vectors — repo · Apache-2.0 · open call for independent runners: implement JCS + SHA-256 from the spec, verify all 78 audit vectors, and get recorded in the registry.

The 223 expression-layer vectors are still waiting for their first independent runner. If you want to prove a standard rather than endorse one — the repo is open.

Determinism isn't declared. It's tested. And in the limit, it's proven.