What should a policy decision prove, and to whom? Three questions from wiring an ADR-0015 backend

[Wyatt Benno (wyattbenno777)]

I am currently writing a research post on verification layers for agent governance, formal methods, and cryptography.

Doing so I built an ExternalPolicyBackend for our tool ICME PreFlight (ICME-Lab/icme-agt, conformance-tested against PolicyEvaluator in CI) and integrated it with the 01-loan-processing MAF scenario.

Three questions came out of it. Related: #276.

Q1: Can you govern actions that have no schema? OPA and Cedar evaluate structured requests, which presumes a principal/action/resource model already exists. But "green-light three fundings of eighty thousand dollars each for applicant C-104 today" is $240k of structured same-day funding, passes every deny regex in the stock scenario, and has no schema. PreFlight's answer: compile natural-language policy to SMT, extract typed variables from the natural-language action at check time, solve. Is "no schema yet" a gap the backend tier should own?

Q2: What is proof_artefact actually for? Cedar's formal verification proves the evaluator is correct in general. It proves nothing about any specific decision: an auditor still has to trust your logs that this check really ran, against this policy, and returned this result. BackendDecision.proof_artefact looks like the field meant to close that gap by attaching evidence to each decision, but no in-tree backend populates it. PreFlight fills it with a per-decision ZK proof (JOLT-based zkML) anyone can verify at a public endpoint, no account needed. Is per-decision evidence what the ADR-0015 authors intended this field for?

Q3: Can a decision be verified by someone not allowed to read the policy? Verifying Rego or Cedar requires reading the rules. A ZK proof could show the decision followed the policy without disclosing it: a bank proves an agent's action satisfied internal risk rules, rules stay private. In scope for verification_pointers? This works well for SMT backed proofs in our repo.

Trade-offs: probabilistic extraction in front of the solver (mitigated by dual LLM+Z3 verification, fail-closed defaults), ~1s latency, per-check cost. Escalation tier, not fast path.

Field note: the scenario's catch-all audit_all_actions rule is terminal-allow and matches every context, so no registered backend, including in-tree OPABackend and CedarBackend, can ever fire in it. Happy to paste a 12-line repro or PR fixes, but the questions are why we're here.

Working fork with the allow-to-block delta, real MAF agent, unmodified maf_adapter, captured live run: examples/maf-loan-act5.

(Community ADR-0015 implementation, not affiliated with Microsoft. Research post to follow.)

[AlgoVoi (Christopher Hopley) (chopmob-cloud)]

These are the right three questions, and the core of Q2 and Q3 is already addressed in-tree, just not where the v4 field sits. Worth pointing at policy-engine/spec/agt/AGT-EVIDENCE-1.0.md, since it looks like the thing you are reaching for.

On Q2: that spec makes per-decision evidence first class. evidence_artefact plus verification_pointers ride on the verdict, and it states they are the successor to the v4 BackendDecision.proof_artefact and verification_pointers you are populating, semantics unchanged, with only the carrier moved from the backend-decision wrapper onto the verdict and telemetry. So per-decision evidence is what that field is for, and the direction you inferred matches the spec rather than fighting it. It also lists reference dispatchers, including a TEE-SGX one that emits an artefact and a verification_pointers.attestation_endpoint, so at least one evidence-emitting path is already sketched. A per-decision ZK backend slots into exactly that dispatcher plus pointer shape.

On Q3: the same model answers it. verification_pointers keys are documented per dispatcher, and a verifier consumes evidence through the pointer rather than by reading the rules, which the TEE attestation endpoint already assumes. A ZK proof is the same slot with a stronger property: it shows the decision satisfied the policy without disclosing the policy, where the TEE path discloses to the enclave instead. So policy-private verification is in scope for verification_pointers; it reads as another dispatcher, not a new mechanism.

On Q1, one caution that ties back to Q2. Compiling natural language to SMT and extracting typed variables at check time puts the extraction in the trusted computing base. The proof then attests that the solver was correct on the extracted typed action, not that the extracted action faithfully represents the natural-language one. Dual LLM and Z3 checking with fail-closed defaults lowers the extraction error rate but does not remove it from what has to be trusted. The move that closes it is the same move as Q2: seal the extracted typed action into the evidence artefact itself, so a verifier sees the exact typed interpretation the decision ran against and can judge the extraction rather than trust it. That turns "trust our extraction" into "here is the interpretation we bound and proved against."

The audit_all_actions terminal-allow shadowing every registered backend, if it behaves as you describe, is a separable issue worth landing the 12-line repro as its own PR regardless of where the three questions go.

On what the ADR-0015 and AGT-EVIDENCE authors actually intended, that is theirs to confirm. The above is an implementer's read of where the fields and the dispatcher model already point.