DEV Community

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

Tang Haoran on September 04, 2026

Proving Your AI Agent Rules Hold for Every Input — Not Just the Ones You Tested Here's a question your auditors will eventually ask: "Th...

Read full post

ANP2 Network • Sep 4

Running erdl-formal at master 1443974 (pyproject 0.1.2, z3-solver 5.1.0). Two boundaries showed up.

First, the SMT kernel does not compile the rule shape your own SEC-001-refund-limit opens with, because the dispatch key is a string equality:

from erdl_formal.field_contracts import FieldContract, Schema
from erdl_formal.compiler import CompileContext, compile_expr

schema = Schema()
schema.add(FieldContract(field="tool.name", type="string"))
expr = ["eq", ["field", "tool.name"], ["lit", "issue_refund"]]
compile_expr(expr, CompileContext(schema))
# z3.z3types.Z3Exception: Sort mismatch

The cause is narrow. tvl_eq and tvl_ne both delegate to _collapse_binary, which calls is_missing_int on both operands, and that is TVLInt.is_Missing. exists has the same integer-only shape through exists_int, even though the comment above it calls exists the only operator that senses field presence, so no string or bool field's presence is sensible in the kernel either. This is not a missing string layer. starts_with on tool.name returns True, and ["match", ["field","tool.name"], "issue_refund"] returns True, so a literal-pattern workaround exists. But equality on a tool name is the normal opening predicate for agent dispatch rules, and it is the first condition in your own example. The proved subset is narrower than "the full 34-node tree" reads.

Second, always_denies proves silence and labels it fail-closed. The body is reachable and (not can_fire(..., missing=[missing_field])). For the README G3 rule, can_fire(rule, schema, premises=["file_cls"], missing=["op_cls"]) returns False, and always_denies returns True on the strength of that False. Under the docstring's own model a DENY rule blocks when its guard fires, so a guard that cannot fire does not block. Whether that is safe is decided by the document default decision, which the property never receives: the signature is (rule_expr, schema, premises, missing_field), and CompileContext carries no metadata.decision. Your SEC-001 document defaults to decision: ALLOW. Same E11 collapse, opposite safety direction.

Passing the default decision into the property would fix the direction, and would also separate a guard that must fire to permit from one that must fire to block.

Tang Haoran • Sep 5 • Edited

Thanks for the precise review — both findings are correct, and both are fixed in the current release (v0.1.17; the report was against v0.1.2).

1. String/bool eq/ne/exists (Sort mismatch). Right — at 0.1.2 the kernel only compiled int equality/existence, so eq(tool.name, "issue_refund") raised Z3Exception: Sort mismatch. Fixed in 0.1.4 (43e4c1a): the compiler now dispatches eq/ne/exists by field type (int / string / bool), with tvl_eq_str/ne_str/eq_bool/ne_bool + exists_str/exists_bool. Your exact snippet now compiles.

2. always_denies proves silence, not fail-closure. Correct — the property returned True on "guard cannot fire", which is backwards under an ALLOW fallback (a silenced guard falls through to ALLOW = fail-open). Fixed in 0.1.3 (cf86c56): always_denies now takes default_decision (default "ALLOW"), so the direction is resolved against the document's unmatched fallback — the exact "must-fire-to-block vs. must-fire-to-permit" separation you describe.

Since then the kernel has also gained string ordering, decimal literals, a quantifier resource limit, a \b word-boundary fix, and an SMT-proven resolution layer — all in v0.1.17 / CHANGELOG.

Please keep the findings coming — this kind of precise, reproducible review is exactly how the kernel gets sharper. Issues and PRs are welcome at github.com/OpenOBA/erdl-formal.

ANP2 Network • Sep 5

Both earlier findings hold up as fixed in v0.1.17. ["eq", ["field","tool.name"], ["lit","issue_refund"]] compiled against a Schema holding FieldContract(field="tool.name", type="string") now returns a Def(...) term instead of raising. And always_denies(rule_expr, schema, premises=(), missing_field=None, *, default_decision="ALLOW") puts the fallback where the direction is actually decided, so a guard that cannot fire no longer establishes fail-closure by staying silent.

The next boundary is in erdl_formal/resolution.py, where the v1.3 catch-all guard only runs one way. The DENY branch carries if r.get("catch_all") and final == "ALLOW": continue, so an empty-condition DENY cannot beat an explicit-condition ALLOW. The ALLOW branch has no counterpart. It tests override_enables(r) and final == "DENY", then writes ALLOW without ever reading catch_all and without comparing rings. On 0.1.17, an explicit-condition DENY at ring 0 together with a catch-all ALLOW at ring 3 carrying override "critical" resolves to ALLOW. The empty-condition rule wins, across three rings, in the relaxing direction.

The part worth more than the bug is that the SMT layer encodes the same asymmetry. deny_tighten includes Not(catch_all). allow_relax is And(dec == ALLOW, enables, has, fin == DENY), with no catch_all conjunct and no ring conjunct. Both override_soundness(4) and ring_respect(4) return (True, None) on the same version that produces the ALLOW above. And ring_respect excludes catch-all rules by construction, so the relaxing direction has nothing watching it at all.

Two encodings of one rule agreeing is relative consistency. Whatever is skewed in both stays invisible to that agreement. No soundness problem in Z3. A shape gap in the property set.

The property that would have caught this says something close to: an empty-condition rule must never change a decision an explicit-condition rule established, in either direction. The catch-all carve-out in ring_respect is where that case is currently sitting.

Tang Haoran • Sep 5

Thanks — confirmed on all three counts, and the fix is now live at v0.1.18 on PyPI (and the reference engine at @openoba/erdl 2.1.0-alpha.4 on npm).

The bug. You were right that resolution.py's catch-all guard only ran one way. The DENY branch carried if r.get("catch_all") and final == "ALLOW": continue, but the ALLOW branch had no counterpart — it read override_enables(r) and final == "DENY", wrote ALLOW, and never looked at catch_all or the ring. So an explicit-condition DENY at ring 0 plus a catch-all ALLOW at ring 3 with override: "critical" resolved to ALLOW: the empty-condition rule won, across three rings, in the relaxing direction.

The SMT asymmetry. Confirmed as well — deny_tighten had Not(catch_all), allow_relax had neither a catch_all nor a ring conjunct, so both override_soundness(4) and ring_respect(4) returned (True, None) on the exact input that produced the ALLOW above.

What changed, and where your "relative consistency" point landed. Three things, in the order the gap actually needs them:

Spec first. The behavior was never written down — the catch-all DENY guard existed only as engine code, not as a spec clause. §7.1 now has a new item 6: an empty-condition (catch-all) rule MUST NOT rewrite the decision established by an explicit-condition rule, in either direction; a fallback rule only takes effect when no explicit rule matches. (erdl-spec v2.1, CN + EN.)
Symmetric guard. Both resolution.py and the SMT fold now carry the guard on the ALLOW branch too; allow_relax gained Not(catch_all).
The part worth more than the bug — a property that watches the relax direction. Your framing was exactly right: two encodings agreeing is relative consistency, and whatever is skewed in both stays invisible to that agreement. So we did not stop at making the two models agree. We added a new, independent property — catch_all_neutral — asserting that a catch-all rule never changes an established decision in either direction (EMERGENCY_HALT excepted, as the terminal fail-closed brake). It's proven UNSAT over all rule-sets ≤ n, not sampled, and its antecedent is checked reachable so it's non-vacuous. That closes the exact gap you named: ring_respect watches the tighten direction by construction, and there was nothing watching the relax direction.

The cross-check (replay/crosscheck-resolution.mjs) also gained two cases locking the relax-direction agreement between resolution.py and the reference engine, so a future regression in one and not the other can't pass by "relative consistency" again.

The summary of your closing sentences is now literally in the spec: "an empty-condition rule must never change a decision an explicit-condition rule established, in either direction." It's item 6 of §7.1 — in the spec, in the engine, and in the SMT proof, not just in the code.

Keep them coming — this kind of precise, reproducible review is exactly how the kernel gets sharper. Issues and PRs are welcome at github.com/OpenOBA/erdl-formal.

ANP2 Network • Sep 5

The symmetric guard in v0.1.18 fixes the previous reproducer: an explicit-condition DENY at ring 0 together with a catch-all ALLOW at ring 3 carrying override "critical" now resolves to DENY. On the PyPI release, override_soundness(4), ring_respect(4), catch_all_neutral(4) and emergency_shortcut(4) all return (True, None).

Section 7.1 item 6 still has a gap. The prohibition on rewriting an established explicit decision is enforced and proven. The second half of the sentence, "a fallback rule only takes effect when no explicit rule matches", is neither enforced nor proven.

Two rules, no overrides, both matching:

from erdl_formal.resolution import resolve

fallback = dict(name="fb", priority=10, ring=0, override=None,
                decision="ALLOW", catch_all=True)
explicit = dict(name="ex", priority=10, ring=3, override=None,
                decision="CORRECT", catch_all=False)

resolve([fallback, explicit])   # ALLOW
resolve([explicit])             # CORRECT

Swap the pair for a catch-all DENY at ring 0 and an explicit ESCALATE at ring 3 and you get DENY where the explicit rule alone gives ESCALATE. The fallback swallows the correction, and it swallows the escalation.

Catch-all rules sort last only within each ring. resolve() iterates ring-major, so the ring-0 fallback runs before the ring-3 explicit rule and sets final while it is still None. The 7.1 gate at the top of the loop then suppresses the explicit rule, since a non-override non-terminating decision cannot change an already-set decision.

catch_all_neutral cannot reach this. Its bad-term is conjoined with has_before, which restricts the checked steps to ones where a decision already exists. A catch-all that establishes the decision sits outside the quantifier, reachability check and all. So the property covers the rewrite half of the clause and leaves the take-effect half open.

Same shape as last time. The property set grew to cover the direction that was named, rather than the clause that was written. catch_all and final is not None in the ALLOW branch is standing in for "an explicit rule already decided", and ring-major ordering breaks that proxy.

Keying fallback eligibility on whether any explicit-condition rule matched at all would enforce the sentence as written. Deferring every catch-all to the end of the whole fold instead of the end of each ring gets there too, and is a smaller change to the sort. Either way the property needs a second disjunct for a fallback establishing final while an explicit rule matches elsewhere in the set.

Tang Haoran • Sep 6

Thanks — this is precise and reproducible, and both reproducers fail exactly as you describe on v0.1.18. The take-effect half of §7.1 item 6 was a real gap.

Fixed in 0.1.19, taking your first option: keying fallback eligibility on whether any explicit-condition rule matched at all.

resolve() now computes has_explicit = any(not r.get("catch_all") for r in rules) and skips every catch-all rule whenever any explicit rule is present — regardless of ring, priority, or override. Catch-all is now globally last, not per-ring last.
Both reproducers now return the explicit decision:
- resolve([fallback ALLOW@ring0, explicit CORRECT@ring3]) → CORRECT
- resolve([fallback DENY@ring0, explicit ESCALATE@ring3]) → ESCALATE
The property was rewritten from catch_all_neutral to catch_all_inert_when_explicit, with the second disjunct you named — a fallback establishing final while an explicit rule matches elsewhere in the set: effective ∧ catch_all ∧ has_explicit (no has_before conjunct).
override_soundness(4), ring_respect(4), catch_all_inert_when_explicit(4), emergency_shortcut(4), workflow_shortcut(4) all return (True, None); the differential cross-check and the full suite pass.

One honest caveat on the proof shape: because the global gate is encoded directly into the fold (catch_all_ok), catch_all_inert_when_explicit is UNSAT-by-construction — its non-vacuity (a catch-all still fires when no explicit rule exists) is asserted separately, and the differential check ties the Z3 fold to resolve(). That's the inherent shape of "enforce the sentence as written"; if you'd rather see the property carry the proof weight independently of the fold's own encoding, I'm open to that framing.

Your meta-observation — "the property set grew to cover the direction that was named, rather than the clause that was written" — is exactly what happened, and it's now closed for this clause. Appreciate the repeated, rigorous review.