CAGE: Certified Authorization under Typed-Return Uncertainty for Tool-Using Agents

# Certified Authorization under Typed-Return Uncertainty for Tool-Using Agents
Source: [https://arxiv.org/html/2607.29190](https://arxiv.org/html/2607.29190)
###### Abstract

Tool\-using LLM agents act on typed tool returns, records pairing provenance and categorical fields with numerical values\. Runtime permission gates generally authorize the observed return and action, leaving the decision unprotected against small errors in how the return was bound to its source\. We ask whether a candidate action stays authorized over a declared neighborhood of plausible correctly bound returns: one admissible binding fault plus bounded numerical drift\. We prove that certifying the categorical and numerical channels separately does not compose: perturbations that are safe on each channel alone can jointly turn the same action unsafe\. CAGE certifies this joint neighborhood directly, enumerating the discrete branches exactly and certifying the continuous perturbation within each branch\. Across synthetic, policy\-as\-code, regulatory, and real\-transaction settings, CAGE removes the in\-budget false allows that accurate pointwise gates admit, while keeping a useful fraction of decisions autonomous\. When the policy is executable, CAGE\-Exact certifies the policy itself; otherwise CAGE\-Lip and CAGE\-RS certify a learned gate under an explicit, measured fidelity assumption\.

## 1Introduction

LLM agents operate in a loop \(reason, emit a structured tool request, observe, continue\(Yaoet al\.[2023](https://arxiv.org/html/2607.29190#bib.bib8)\)\), so tool observations become inputs to future actions: external bytes influence control flow\(Greshakeet al\.[2023](https://arxiv.org/html/2607.29190#bib.bib5); Ruanet al\.[2024](https://arxiv.org/html/2607.29190#bib.bib14)\)\. Deployed agent harnesses increasingly place a runtime permission gate between the model and tool execution\(Liuet al\.[2026](https://arxiv.org/html/2607.29190#bib.bib1); Jiet al\.[2026](https://arxiv.org/html/2607.29190#bib.bib2)\); current gates are heuristic, pre\-execution, and defined over the proposed call: they decide whether it may run, and leave open whether the agent may safely act on what it returns\. Existing defenses concentrate on the untrusted text channel: sanitizing or spotlighting tool outputs\(Daset al\.[2025](https://arxiv.org/html/2607.29190#bib.bib9); Hineset al\.[2024](https://arxiv.org/html/2607.29190#bib.bib10)\), structured prompting and instruction hierarchies\(Chenet al\.[2025](https://arxiv.org/html/2607.29190#bib.bib11); Wallaceet al\.[2024](https://arxiv.org/html/2607.29190#bib.bib12)\), and information\-flow control by design\(Debenedettiet al\.[2025](https://arxiv.org/html/2607.29190#bib.bib13)\); these act on the text or data\-flow channel, complementary to the typed authorization decision we certify \(§[6\.3](https://arxiv.org/html/2607.29190#S6.SS3)\)\.

![Refer to caption](https://arxiv.org/html/2607.29190v1/x1.png)Figure 1:Post\-tool\-return authorization boundary\. The LLM reads the validated recordz~=\(s,x\)\\tilde\{z\}=\(s,x\)and untrusted textmm, which can steer the proposalaa; the gate reads only\(z~,a\)\(\\tilde\{z\},a\): the text channel is excluded architecturally; the typed channel is validated, its residual binding uncertainty certified\.Example \(joint\-gap witness\)\.The served record readssource=credit\_check\\texttt\{source\}=\\texttt\{credit\\\_check\},risk\_score=0\.46\\texttt\{risk\\\_score\}=0\.46, and the agent proposesapprove\_transaction; under credit\-check provenance the approval threshold is loose\. The tag is stale: the record was produced by the sanctions screen, whose threshold is strict; the fresh score sits slightly higher, within validation tolerance\. The observed record is safe at the point and passes each single\-channel check; a state it plausibly stands for is not\. The pointwise predicate authorizes the served record; evaluation overBd,εB\_\{d,\\varepsilon\}identifies the unsafe plausible return\.

Existing runtime hooks can host the required decision, but permission gates, runtime enforcers, and LLM judges all evaluate the realized return–action pair pointwise\. We change the object of authorization from the observed point\(z~,a\)\(\\tilde\{z\},a\)to the joint neighborhoodBd,ε​\(z~\)B\_\{d,\\varepsilon\}\(\\tilde\{z\}\): a candidate action is authorized only when it is safe for every correctly bound return inBd,ε​\(z~\)B\_\{d,\\varepsilon\}\(\\tilde\{z\}\)\.

We therefore study the node\(z,a\)↦Allow⁡\(z,a\)\(z,a\)\\mapsto\\operatorname\{Allow\}\(z,a\), wherez=\(s,x\)z=\(s,x\)is a typed tool return andaais a candidate downstream action; the LLM may still proposeaa, and the runtime gate decides whether executing it is authorized under a specified perturbation model, abstention routing the residual to human review\.

The central vulnerability is a joint\-gap attack: a return\-action pair may be clean\-safe at the observed point and pass discrete\-only and continuous\-only checks, yet fail under a joint perturbation, because the discrete part of the return changes the semantics of the numerical fields, as in the screening example above\. We call such points*joint\-gap witnesses*\(categoryCCof the oracle taxonomy\): safe at the observed point and under each marginal check, yet unsafe for some\(s′,x′\)∈Bd,ε​\(s,x\)\(s^\{\\prime\},x^\{\\prime\}\)\\in B\_\{d,\\varepsilon\}\(s,x\)\. The defense, our monitorCAGE\(Certified Authorization Gate for Execution\), certifies the actual joint perturbation set: enumerate the finite discrete neighborhood exactly and certify each continuous branch with a sound backend\. When the policy is executable, CAGE\-Exact certifies it directly; otherwise, CAGE\-Lip or CAGE\-RS certifies a learned gate under a measured fidelity assumption \(Table[2](https://arxiv.org/html/2607.29190#S5.T2)\)\.

#### Contributions\.

- •Robust authorization problem\.We formalize authorization after a tool return as a decision under bounded semantic uncertainty: the runtime observes a validated recordz~\\tilde\{z\}, but the correctly bound return may be anyz⋆∈Bd,ε​\(z~\)z^\{\\star\}\\in B\_\{d,\\varepsilon\}\(\\tilde\{z\}\)\. Proposition[1](https://arxiv.org/html/2607.29190#Thmproposition1)establishes that return\-dependent safety requires reading the realized return \(≈44%\\approx 44\\%of matched pairs, Section[6\.2](https://arxiv.org/html/2607.29190#S6.SS2)\); CAGE replaces pointwise evaluation with certification over the full joint neighborhood \(Figure[2](https://arxiv.org/html/2607.29190#S2.F2)\)\.
- •Non\-composition\.We prove separate certificates for the categorical and numerical channels do not imply safety over their Cartesian product \(Theorem[1](https://arxiv.org/html/2607.29190#Thmtheorem1)\): joint\-gap witnesses are safe at the observed point and under each marginal perturbation, yet unsafe for a combined move; the witness interval has lengthmin⁡\(Δ,ε\)\\min\(\\Delta,\\varepsilon\)and the empirical witness frequency follows this geometry \(Section[6\.2](https://arxiv.org/html/2607.29190#S6.SS2)\)\.
- •Certified monitor with an assumption ladder\.CAGE enumerates𝒩d​\(s\)\\mathcal\{N\}\_\{d\}\(s\)exactly and certifies each branch by a backend from an assumption ladder, with a backend\-independent abstention floor \(Proposition[3](https://arxiv.org/html/2607.29190#Thmproposition3)\)\. For the learned rungs, the certificate is over the gate; it is policy\-sound under an explicit gate–policy fidelity condition, measured throughout the evaluation\.
- •Measured safety case\.We calibrate the discrete and continuous budgets from injected return\-assembly faults, derive a deployment\-specific freshness limit, and evaluate adaptive attacks and policy shift\. The formal guarantee is separated from its operational preconditions and residual risk; external\-validity claims concern existence, mechanism, and frequency within the evaluated settings, and field prevalence is not measured\.

## 2Background and Related Work

The harness owns the agent loop’s security\-relevant boundaries, the raw model reduced to a proposer\(Yaoet al\.[2023](https://arxiv.org/html/2607.29190#bib.bib8); Liuet al\.[2026](https://arxiv.org/html/2607.29190#bib.bib1)\)\(extended background: Appendix B\)\. Deployed permission systems sit at those boundaries but are almost entirely*pre\-execution*; a recent stress test reports the same state\-changing effect reachable through an unevaluated path\(Jiet al\.[2026](https://arxiv.org/html/2607.29190#bib.bib2)\)\.*Indirect prompt injection*and tool/description poisoning\(Greshakeet al\.[2023](https://arxiv.org/html/2607.29190#bib.bib5); Zhanet al\.[2024](https://arxiv.org/html/2607.29190#bib.bib6); Debenedettiet al\.[2024](https://arxiv.org/html/2607.29190#bib.bib7); Wanget al\.[2026b](https://arxiv.org/html/2607.29190#bib.bib16)\)are a*different stage*: there adversarial bytes steer the model, whereas we assume a tool has already returned a typed object and ask whether acting on it is authorized\.

#### Certified robustness\.

Two certification families transfer to typed authorization\.*Lipschitz\-margin certification*certifies any decision whose margin exceedsL​εL\\varepsilon\(Tsuzukuet al\.[2018](https://arxiv.org/html/2607.29190#bib.bib35)\), with expressive11\-Lipschitz architectures built from orthogonal layers\(Anilet al\.[2019](https://arxiv.org/html/2607.29190#bib.bib36); Trockman and Kolter[2021](https://arxiv.org/html/2607.29190#bib.bib37)\); it is our primary learned backend \(CAGE\-Lip, Section[5\.1](https://arxiv.org/html/2607.29190#S5.SS1)\)\.*Randomized smoothing*gives model\-agnostic guarantees under continuous perturbations for black\-box classifiers\(Cohenet al\.[2019](https://arxiv.org/html/2607.29190#bib.bib3)\), with extensions to conformal prediction\(Zargarbashiet al\.[2025](https://arxiv.org/html/2607.29190#bib.bib4)\); it backs CAGE\-RS\. Enumerate\-then\-certify parallels certified word\-substitution defenses\(Jiaet al\.[2019](https://arxiv.org/html/2607.29190#bib.bib48); Huanget al\.[2019](https://arxiv.org/html/2607.29190#bib.bib49)\)\. Smoothing an LLM*transcript*classifier is infeasible \(high\-dimensional, discrete, semantically unstable\); typed returns are favorable: low\-dimensional continuous fields, small𝒩d​\(s\)\\mathcal\{N\}\_\{d\}\(s\)\(88–1818atd=1d=1, Table S29\)\. Hybrid and discrete smoothing kernels\(Leeet al\.[2019](https://arxiv.org/html/2607.29190#bib.bib50); Bojchevskiet al\.[2020](https://arxiv.org/html/2607.29190#bib.bib51)\)pay discrete Monte\-Carlo variance and win only when𝒩d​\(s\)\\mathcal\{N\}\_\{d\}\(s\)is too large to enumerate*and*the gate is black\-box; neither holds here \(Proposition 4\)\. The technical components build on established certification methods; the contribution lies in the joint\-neighborhood authorization formulation, the non\-composition result, and the measured safety case\.

#### Runtime enforcement, verification, and what stays uncertified\.

![Refer to caption](https://arxiv.org/html/2607.29190v1/x2.png)Figure 2:Two axes place the post\-tool\-return node:*evaluation locus*\(the observed point vs\. the bounded neighborhoodBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\)\) and*policy*\(executable predicate vs\. learned from labels\); our monitor occupies the neighborhood row, off\-axis defenses the text channel, tool descriptions, or training data\.Two axes separate our node from recent agent\-security work \(Figure[2](https://arxiv.org/html/2607.29190#S2.F2)\): whether a defense reads the typed pair\(z,a\)\(z,a\), and whether it is*certified*under bounded uncertainty between the validated record and its correctly bound return\. A growing line of*runtime enforcement*reads the action and checks it against a policy but offers no uniform guarantee over bounded semantic return uncertainty: VeriGuard formally verifies a synthesized policy and runs a per\-action monitor\(Miculicichet al\.[2025](https://arxiv.org/html/2607.29190#bib.bib25)\); AgentSpec enforces trigger/predicate/enforcement rules with no trajectorial analysis\(Wanget al\.[2026a](https://arxiv.org/html/2607.29190#bib.bib26)\); PFI and SAFEFLOW import OS\-style isolation and information\-flow control\(Kimet al\.[2025](https://arxiv.org/html/2607.29190#bib.bib27); Liet al\.[2025](https://arxiv.org/html/2607.29190#bib.bib28)\)\. These runtime defenses evaluate the observed action–state pair and do not provide a certificate uniform overBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\); CAGE provides this uniform neighborhood certificate, while the runtime placement follows this enforcement line\. The certified line targets*different*corruptions, adversarial tool*descriptions*\(ToolCert\(Yeonet al\.[2025](https://arxiv.org/html/2607.29190#bib.bib17)\)\) and*training\-set*poisoning \(TPA\(Ghitu and Wicker[2026](https://arxiv.org/html/2607.29190#bib.bib30)\)\); neither addresses certification overBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\)at inference, an open surface in a recent SoK\(Linget al\.[2026](https://arxiv.org/html/2607.29190#bib.bib29)\)\. Beyond agent security, access\-control policy verification\(Fisleret al\.[2005](https://arxiv.org/html/2607.29190#bib.bib43)\), attribute\-based access control\(Huet al\.[2014](https://arxiv.org/html/2607.29190#bib.bib52)\), runtime shielding\(Alshiekhet al\.[2018](https://arxiv.org/html/2607.29190#bib.bib44)\), and robust optimization\(Ben\-Talet al\.[2009](https://arxiv.org/html/2607.29190#bib.bib45)\)verify, enforce, or optimize the policy itself; CAGE certifies the authorization*decision*overBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\)at inference\. Our safety predicate follows the oracle\-function formalization of agent security\(Siuet al\.[2026](https://arxiv.org/html/2607.29190#bib.bib31)\), realized with a typed gate, since LLM judges measure adversarial robustness no better than chance under shift\(Schwinnet al\.[2026](https://arxiv.org/html/2607.29190#bib.bib32)\)\.

## 3Problem Setting

What exactly is the task?Given a validated typed tool returnz~\\tilde\{z\}and an actionaaproposed by the agent, decide whetheraaremains authorized for*every*plausible correctly bound returnz′∈Bd,ε​\(z~\)z^\{\\prime\}\\in B\_\{d,\\varepsilon\}\(\\tilde\{z\}\)\.Observed return:source=credit\_check\\texttt\{source\}=\\texttt\{credit\\\_check\},score=0\.46\\texttt\{score\}=0\.46Proposed action:approve\_transactionPolicy:thescorethreshold depends on thesourceUncertainty:one source\-binding error and bounded score drift

### 3\.1Typed tool returns

We model a structured tool return asz=\(s,x\)z=\(s,x\), wheres∈𝒮s\\in\\mathcal\{S\}is the discrete part \(tool identity, provenance, categorical fields, status labels\) andx∈ℝkx\\in\\mathbb\{R\}^\{k\}the continuous part \(risk scores, amounts, latencies, prices\)\.

The agent proposes a candidate downstream actiona∈𝒜a\\in\\mathcal\{A\}; the policy oracle is an action\-indexed predicateSafe⁡\(z,a\)∈\{0,1\}\\operatorname\{Safe\}\(z,a\)\\in\\\{0,1\\\}, and the same return may be safe formanual\_reviewyet unsafe forapprove\_transaction\.

### 3\.2Threat model

The gate reads an observed recordz~=\(s,x\)\\tilde\{z\}=\(s,x\): typed, schema\-validated, integrity\- and freshness\-checked\. The record is syntactically valid at decision time; residual uncertainty concerns its binding to provenance, fresh values, and policy state\. The state this record binds to \(the provenance in force, the fresh score, the resolved policy pack\) is denotedz⋆z^\{\\star\}; assembly by adapters, caches, and schema migrations meansz⋆=\(s′,x′\)z^\{\\star\}=\(s^\{\\prime\},x^\{\\prime\}\)may differ fromz~\\tilde\{z\}only within the validated envelope

Bd,ε​\(s,x\)=\{\(s′,x′\):Ddisc​\(s,s′\)≤d,‖x′−x‖2≤ε\}\.B\_\{d,\\varepsilon\}\(s,x\)=\\left\\\{\(s^\{\\prime\},x^\{\\prime\}\):D\_\{\\mathrm\{disc\}\}\(s,s^\{\\prime\}\)\\leq d,\\ \\\|x^\{\\prime\}\-x\\\|\_\{2\}\\leq\\varepsilon\\right\\\}\.
The certified object isAllow⁡\(z~,a\)=1⇒∀z⋆∈Bd,ε​\(z~\):Safe⁡\(z⋆,a\)=1\\operatorname\{Allow\}\(\\tilde\{z\},a\)=1\\Rightarrow\\forall z^\{\\star\}\\in B\_\{d,\\varepsilon\}\(\\tilde\{z\}\):\\ \\operatorname\{Safe\}\(z^\{\\star\},a\)=1: robust authorization under bounded semantic return uncertainty; hereafter we writezzfor the observed record\. The discrete component ofBd,εB\_\{d,\\varepsilon\}captures the small admissible*binding*faults of that assembly \(a stale provenance tag, a confused policy pack, a read\-then\-act race\)\. The continuous component captures the residual numerical uncertainty left after ordinary validation\. Fully fabricated identities, compromised endpoints, and values outside the declared radius are outside the certificate \(Table S32\); the typed constructor and validation stack sit in the trusted computing base \(TCB; Appendix C\)\. The budget is two\-layered: integrity\+freshness validation*enforces*it against adaptive attackers;ε\\varepsilonis a p95 residual*calibrated*on the tested fault process \(Section[6\.5](https://arxiv.org/html/2607.29190#S6.SS5)\);d=1d=1is the measured single\-fault granularity \(d=2d=2recommended against fault\-inducing adversaries; Tables S28–S29\)\.

### 3\.3Two channels: typed return and untrusted display text

In deployment the model consumeso=\(z,m\)o=\(z,m\), validated record plus attacker\-influenced text: two threat models follow \(Figure[1](https://arxiv.org/html/2607.29190#S1.F1)\)\. TM1 \(untrusted text channel\):the adversary controlsmmbut notzz;mmcan move the LLM proposal, but a gate reading onlyzzhasAllow⁡\(z,a\)\\operatorname\{Allow\}\(z,a\)independent ofmm*by construction*: the defense is architectural; any typed gate excludingmminherits it \(cross\-action mis\-selection keeps a0\.310\.31residual, Table S33\)\. TM2 \(bounded semantic return uncertainty\):the runtime observes the validated recordzz, while the correctly bound return may be anyz⋆∈Bd,ε​\(z\)z^\{\\star\}\\in B\_\{d,\\varepsilon\}\(z\); excludingmmno longer suffices; authorization must hold uniformly overBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\)\.

### 3\.4Return\-dependent authorization requires observing the return

The requirement is independent of any certificate machinery\.

###### Proposition 1\(Return dependence\)\.

Suppose there exist two possible tool returnsz0,z1z\_\{0\},z\_\{1\}and a candidate actionaasuch thatSafe⁡\(z0,a\)=1\\operatorname\{Safe\}\(z\_\{0\},a\)=1andSafe⁡\(z1,a\)=0\\operatorname\{Safe\}\(z\_\{1\},a\)=0\. Then any authorization rule that does not inspect the realized returnzzcannot correctly authorizeaain both cases\.

The elementary proof is in Appendix A\. Proposition[1](https://arxiv.org/html/2607.29190#Thmproposition1)locates the decision after the return becomes available, and existing runtime hooks can implement it; Section[6\.2](https://arxiv.org/html/2607.29190#S6.SS2)measures how often return dependence occurs\.

Table 1:Notation used throughout\.

## 4Why Marginal Certificates Do Not Compose

A natural baseline certifies the two channels separately and allows if both marginal certificates pass; this is unsound\. A continuous certificate at the original discrete state proves∀x′∈Bε​\(x\):Safe⁡\(\(s,x′\),a\)=1\\forall x^\{\\prime\}\\in B\_\{\\varepsilon\}\(x\):\\operatorname\{Safe\}\(\(s,x^\{\\prime\}\),a\)=1, and a discrete certificate at the original numerical value proves∀s′∈𝒩d​\(s\):Safe⁡\(\(s′,x\),a\)=1\\forall s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\):\\operatorname\{Safe\}\(\(s^\{\\prime\},x\),a\)=1, but the needed joint statement is strictly stronger:

\[∀x′∈Bε​\(x\):Safe⁡\(\(s,x′\),a\)=1\]\\displaystyle\\bigl\[\\forall x^\{\\prime\}\\in B\_\{\\varepsilon\}\(x\):\\operatorname\{Safe\}\(\(s,x^\{\\prime\}\),a\)=1\\bigr\]∧\\displaystyle\\land\\quad\[∀s′∈𝒩d​\(s\):Safe⁡\(\(s′,x\),a\)=1\]\\displaystyle\\bigl\[\\forall s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\):\\operatorname\{Safe\}\(\(s^\{\\prime\},x\),a\)=1\\bigr\]⇏\\displaystyle\\nRightarrow\\quad\[∀s′∈𝒩d​\(s\),∀x′∈Bε​\(x\):Safe⁡\(\(s′,x′\),a\)=1\]\.\\displaystyle\\bigl\[\\forall s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\),\\,\\forall x^\{\\prime\}\\in B\_\{\\varepsilon\}\(x\):\\operatorname\{Safe\}\(\(s^\{\\prime\},x^\{\\prime\}\),a\)=1\\bigr\]\.The joint\-gap attack occupies exactly this logical gap: the unsafe region exists only in the discrete–continuous interaction\.

###### Theorem 1\(Non\-composition of marginal certificates\)\.

There exist safety predicatesSafe\\operatorname\{Safe\}, points\(s,x\)\(s,x\), actionsaa, discrete neighborhoods𝒩d​\(s\)\\mathcal\{N\}\_\{d\}\(s\), and continuous ballsBε​\(x\)B\_\{\\varepsilon\}\(x\)such thatSafe⁡\(\(s,x′\),a\)=1\\operatorname\{Safe\}\(\(s,x^\{\\prime\}\),a\)=1for allx′∈Bε​\(x\)x^\{\\prime\}\\in B\_\{\\varepsilon\}\(x\)andSafe⁡\(\(s′,x\),a\)=1\\operatorname\{Safe\}\(\(s^\{\\prime\},x\),a\)=1for alls′∈𝒩d​\(s\)s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\), yetSafe⁡\(\(s′,x′\),a\)=0\\operatorname\{Safe\}\(\(s^\{\\prime\},x^\{\\prime\}\),a\)=0for somes′∈𝒩d​\(s\)s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\),x′∈Bε​\(x\)x^\{\\prime\}\\in B\_\{\\varepsilon\}\(x\)\.

With one\-dimensionalxxand a threshold that shifts byΔ\\Deltaacross the swap, continuous\-only safety needsx≤q−εx\\leq q\-\\varepsilonand discrete\-only safety needsx≤q−Δx\\leq q\-\\Delta, yet the joint move is unsafe forx\>q−Δ−εx\>q\-\\Delta\-\\varepsilon; all three hold exactly on the witness interval\(q−Δ−ε,min⁡\(q−ε,q−Δ\)\]\\bigl\(q\-\\Delta\-\\varepsilon,\\ \\min\(q\-\\varepsilon,q\-\\Delta\)\\bigr\]of lengthmin⁡\(Δ,ε\)\\min\(\\Delta,\\varepsilon\)\(Figure[3](https://arxiv.org/html/2607.29190#S5.F3); proof in Appendix A\)\. The prevalence ofCCtherefore scales asmin⁡\(Δ,ε\)\\min\(\\Delta,\\varepsilon\)\(measured in Section[6\.2](https://arxiv.org/html/2607.29190#S6.SS2)\)\.

## 5Method

CAGE certifies the actual joint perturbation set: enumerate the finite discrete neighborhood𝒩d​\(s\)=\{s′:Ddisc​\(s,s′\)≤d\}\\mathcal\{N\}\_\{d\}\(s\)=\\\{s^\{\\prime\}:D\_\{\\mathrm\{disc\}\}\(s,s^\{\\prime\}\)\\leq d\\\}exactly, run a sound per\-branch test on the continuous ball at everys′s^\{\\prime\}, and allow only when every branch passes,

AllowCAGE⁡\(s,x,a\)=1⇔mins′∈𝒩d​\(s\)⁡Certε​\(s′,x,a\)=1\.\\operatorname\{Allow\}\_\{\\mathrm\{CAGE\{\}\}\}\(s,x,a\)=1\\iff\\min\_\{s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)\}\\mathrm\{Cert\}\_\{\\varepsilon\}\(s^\{\\prime\},x,a\)=1\.A certified allow covers every branch under the continuous budget, up to the branch test’s stated confidence: exactly the joint budget the joint\-gap attack exploits\. Each branch is read as a plausible correctly bound returnz⋆∈Bd,ε​\(z\)z^\{\\star\}\\in B\_\{d,\\varepsilon\}\(z\)\(TM2, Section[3\.3](https://arxiv.org/html/2607.29190#S3.SS3)\)\. The branch testCertε\\mathrm\{Cert\}\_\{\\varepsilon\}comes from the assumption ladder of Section[5\.1](https://arxiv.org/html/2607.29190#S5.SS1)\.

Table 2:What each backend certifies: rung 1 is*policy\-certified*; rungs 2–3 and the ceiling are*gate\-certified*, policy\-sound under measured fidelity\. Every result is one of: policy certificate / gate certificate / oracle\-measured fidelity \(cert\_false\_allow, henceforth CFA\) / out\-of\-budget escape \(Section[6\.5](https://arxiv.org/html/2607.29190#S6.SS5)\)\.Worked example\.For the screening example, takeq=0\.60q=0\.60,Δ=0\.08\\Delta=0\.08,ε=0\.10\\varepsilon=0\.10; the observed record\(credit\_check,0\.46\)\(\\texttt\{credit\\\_check\},0\.46\)is then a joint\-gap witness:0\.46≤q−ε0\.46\\leq q\-\\varepsilonand0\.46≤q−Δ0\.46\\leq q\-\\Delta, yet0\.46\>q−Δ−ε0\.46\>q\-\\Delta\-\\varepsilon\. CAGE\-Exact enumerates𝒩d​\(s\)=\{credit\_check,sanctions\_screen\}\\mathcal\{N\}\_\{d\}\(s\)=\\\{\\texttt\{credit\\\_check\},\\texttt\{sanctions\\\_screen\}\\\}and runs the rung\-1 test on each branch:0\.46\+0\.10=0\.56≤0\.600\.46\+0\.10=0\.56\\leq 0\.60certifies thecredit\_checkbranch, but0\.56\>0\.520\.56\>0\.52fails thesanctions\_screenbranch\. The minimum over branches is0: the action is therefore refused and routed to review, consistent with Proposition[3](https://arxiv.org/html/2607.29190#Thmproposition3)\.

### 5\.1Certification backends: an assumption ladder

The monitor’s discrete channel is*always*exact enumeration over the joint budgetBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\); only the continuous branch test varies along an*assumption ladder*\(Table[2](https://arxiv.org/html/2607.29190#S5.T2)\): each rung relaxes a requirement on the gate and pays a characterized slack over the soundness floor\. When the policy is implicit we train a binary action\-indexed gate on typed returns and oracle labels: a11\-Lipschitz signed\-margin networkhθh\_\{\\theta\}\(orthogonal layers\(Boissinet al\.[2025](https://arxiv.org/html/2607.29190#bib.bib42)\),Lcert=1L\_\{\\mathrm\{cert\}\}=1\) for rung 2, or Gaussian smoothing of a black\-box gate for rung 3 \(Appendix D\)\. Rung 1 allows iff every affine constraint of every branch passes the exact testw⊤​x\+ε​‖w‖2≤b​\(s′,a\)w^\{\\top\}x\+\\varepsilon\\\|w\\\|\_\{2\}\\leq b\(s^\{\\prime\},a\), inO​\(\|𝒩d​\(s\)\|​m​k\)O\(\|\\mathcal\{N\}\_\{d\}\(s\)\|\\,mk\)over a*verified affine fragment*\(Definition 1, Proposition 7\)\. Rung 2 allows iffmins′∈𝒩d​\(s\)⁡hθ​\(s′,x,a\)\>Lcert​ε\\min\_\{s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)\}h\_\{\\theta\}\(s^\{\\prime\},x,a\)\>L\_\{\\mathrm\{cert\}\}\\varepsilon; rung 3 iffmins′∈𝒩d​\(s\)⁡p¯​\(s′,x,a\)≥τ\\min\_\{s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)\}\\underline\{p\}\(s^\{\\prime\},x,a\)\\geq\\tau\. An out\-of\-fragment policy is detected syntactically and routed to the ceiling or a gate\-certified rung, never silently approximated\. We reserve*policy\-certified*for rung 1 and call rungs 2–3 \(and the ceiling\)*gate\-certified*\.

CAGE\-Exact applies when the policy is executable\. CAGE\-Lip is the default learned backend for implicit policies, while CAGE\-RS provides a conservative fallback for black\-box gates and bounded batches\. Certification of a learned gate does not establish policy correctness; gate–policy fidelity is evaluated separately\. CAGE\-RS’s smoothed certificate reduces empirical policy exposure without removing the fidelity assumption, and its per\-decision confidence fails over a deployment horizon \(Table S47\)\. The complete verification / MILP ceiling \(CROWN\-style verifier\(Zhanget al\.[2018](https://arxiv.org/html/2607.29190#bib.bib39)\)when available; our reported run uses MILP\(Tjenget al\.[2019](https://arxiv.org/html/2607.29190#bib.bib40)\)\) is the offline audit rung: it certifies the trained gate’s*entire*robust\-safe set, identifying whether a low allow rate stems from the learned margin or from the certification backend \(Table S6\)\. WhereSafe\\operatorname\{Safe\}is executable, rung 1 dominates and the learned rungs serve as ablations; their practical role is the implicit\-policy regime, where an executable predicate does not exist by construction \(Section[6\.4](https://arxiv.org/html/2607.29190#S6.SS4)\)\.

### 5\.2Guarantees

The guarantees rely on three properties \(proofs in Appendix A\); define the worst\-branch joint marginm\(z,a\)=mins′∈𝒩d​\(s\)inf\{∥x′−x∥2:Safe\(\(s′,x′\),a\)=0\}m\(z,a\)=\\min\_\{s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)\}\\inf\\\{\\\|x^\{\\prime\}\-x\\\|\_\{2\}:\\operatorname\{Safe\}\(\(s^\{\\prime\},x^\{\\prime\}\),a\)=0\\\}, so the robust\-safe set isR=\{m\>ε\}R=\\\{m\>\\varepsilon\\\}\.

- •Exact enumeration with per\-branch bounds is a valid*joint*discrete–continuous certificate, with no Monte\-Carlo error on the discrete channel \(Proposition 4\)\.
- •The Lipschitz margin test certifies the learned gate’s positive decision over the whole joint ball \(Proposition[2](https://arxiv.org/html/2607.29190#Thmproposition2)\)\.
- •Any sound gate must abstain near the unsafe boundary \(Proposition[3](https://arxiv.org/html/2607.29190#Thmproposition3)\)\.

###### Proposition 2\(Lipschitz\-margin certificate\)\.

IfAllowLip⁡\(z,a\)=1\\operatorname\{Allow\}\_\{\\mathrm\{Lip\}\}\(z,a\)=1, thenhθ​\(s′,x′,a\)\>0h\_\{\\theta\}\(s^\{\\prime\},x^\{\\prime\},a\)\>0for every\(s′,x′\)∈Bd,ε​\(z\)\(s^\{\\prime\},x^\{\\prime\}\)\\in B\_\{d,\\varepsilon\}\(z\): the learned gate’s positive decision is certified over the whole joint budget\.

###### Proposition 3\(Soundness requires boundary abstention\)\.

If a gate is*sound*forBd,εB\_\{d,\\varepsilon\}\(Allow⁡\(z,a\)=1⇒Safe⁡\(z′,a\)=1\\operatorname\{Allow\}\(z,a\)=1\\Rightarrow\\operatorname\{Safe\}\(z^\{\\prime\},a\)=1for allz′∈Bd,ε​\(z\)z^\{\\prime\}\\in B\_\{d,\\varepsilon\}\(z\)\), thenAllow⁡\(z,a\)=1⇒m​\(z,a\)≥ε\\operatorname\{Allow\}\(z,a\)=1\\Rightarrow m\(z,a\)\\geq\\varepsilon, strict when the unsafe set is closed; hencePr⁡\[Allow=1\]≤Pr⁡\[m≥ε\]\\Pr\[\\operatorname\{Allow\}=1\]\\leq\\Pr\[m\\geq\\varepsilon\], with equality for the oracle robust gate up to the boundary\{m=ε\}\\\{m=\\varepsilon\\\}\(empirical mass≈10−5\\approx 10^\{\-5\}; Appendix A\)\. Every joint\-gap witness, and every point strictly within worst\-branch marginε\\varepsilonof the unsafe set, is refused by*any*sound mechanism\.

![Refer to caption](https://arxiv.org/html/2607.29190v1/x3.png)Figure 3:Geometry of a joint\-gap witness: safe at the point and under each marginal check, yet the joint move \(provenance swap \+ continuous shift\) crosses the shifted thresholdq−Δq\-\\Delta; every such point lies withinε\\varepsilonof the unsafe set, so any sound gate must refuse it \(Proposition[3](https://arxiv.org/html/2607.29190#Thmproposition3)\)\.This backend\-independent floor unifies the ladder: rung 1 attains it, rungs 2–3 approach it by the slack column of Table[2](https://arxiv.org/html/2607.29190#S5.T2); CFA measures the gate\-overestimation failure \(Propositions 5–6, Table S6\)\.

## 6Experiments

The evaluation first establishes the existence of joint\-gap witnesses \(Tables[5](https://arxiv.org/html/2607.29190#S6.T5)–[6](https://arxiv.org/html/2607.29190#S6.T6)\), then measures the soundness–autonomy trade\-off \(Table[7](https://arxiv.org/html/2607.29190#S6.T7)\), and finally tests whether the logical gap produces committed side effects \(§[6\.3](https://arxiv.org/html/2607.29190#S6.SS3)\)\. Additional experiments test whether these results depend on judge capacity, the analytic oracle, the attack strategy, policy stationarity, or the assumed budget \(d,εd,\\varepsilon, freshness\)\. The certificate covers a single decisionAllow⁡\(z,a\)\\operatorname\{Allow\}\(z,a\)under the declared budget \(d=1d\{=\}1,ε=0\.10\\varepsilon\{=\}0\.10; §[6\.5](https://arxiv.org/html/2607.29190#S6.SS5)\); rung 1 is policy\-certified, rungs 2–3 are gate\-certified under measured fidelity, and the LLM remains an uncertified proposer\. Section[7](https://arxiv.org/html/2607.29190#S7)discusses the assumptions outside this guarantee\.

Table 3:Experiment map\. Each setting is named by its input data, its policy or oracle, its execution substrate, and its scientific role, so that “real” is never ambiguous between real data, a real engine, a third\-party policy, and real execution\.### 6\.1Setup

Table[3](https://arxiv.org/html/2607.29190#S6.T3)maps each setting to its data, policy, and role; Table[4](https://arxiv.org/html/2607.29190#S6.T4)fixes the shared frame; secondary sweeps live in Appendix E\. The oracle stratifies each pair by where inBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\)safety can flip\. We focus on three categories:UU, unsafe already at the observed point;CC, safe under each marginal check yet unsafe under the joint move \(Theorem[1](https://arxiv.org/html/2607.29190#Thmtheorem1)’s witnesses\); andRR, robust everywhere in the budget\. CategoryCCtests soundness; categoryRRtests non\-vacuity\. We useAA/BBfor stratification only\. We reportCallow,Uallow,Rallow=Pr⁡\[Allow=1∣C,U,R\]C\_\{\\mathrm\{allow\}\},U\_\{\\mathrm\{allow\}\},R\_\{\\mathrm\{allow\}\}=\\Pr\[\\operatorname\{Allow\}=1\\mid C,U,R\]and the oracle\-measured CFA, a certified allow the oracle deems joint\-unsafe\. RS parameters are fixed across experiments \(Appendix D\)\.

Table 4:Shared experimental frame\. Sampling modes: natural, boundary\-balanced \(tagged stress tests\),CC\-targeted \(Table S1\)\.
### 6\.2Return dependence and pointwise authorization

Question\.*How often does authorization depend on the return, and how often do point checks admit joint\-gap witnesses?* Setup\.Matched pairs sharing domain, action, and schema \(10,00010\{,\}000/domain, analytic oracle; generator\-conditional rates\)\. Result\.Return\-dependent pairs span42\.542\.5–45\.6%45\.6\\%across finance/SRE/ops, so any return\-blind rule errs on the minority class \(majority error31\.631\.6–34\.0%34\.0\\%\)\. A learned pre\-return baseline errs2828–33%33\\%, a post\-return gate0\.40\.4–0\.7%0\.7\\%\. Interpretation\.A pre\-return rule cannot distinguish these cases; a post\-return gate can \(Proposition[1](https://arxiv.org/html/2607.29190#Thmproposition1)\)\.

Table 5:Point vs\. neighborhood on the Proposition[3](https://arxiv.org/html/2607.29190#Thmproposition3)witness setW=\{clean\-safe\}∖RW=\\\{\\text\{clean\-safe\}\\\}\\setminus R\(real IEEE\-CIS \+ OPA policy;6032/10,0006032/10\{,\}000\)\. CFA is the joint\-unsafe fraction of*all*certified allows in the run, not ofWW\.†CAGE\-Lip is gate\-certified; the nonzero entry is a base\-gate fidelity caveat\.Because every element ofWWis safe at the observed point by construction, point accuracy is not informative on this set\. Table[5](https://arxiv.org/html/2607.29190#S6.T5)instead distinguishes gates that evaluate the observed point from gates that certify the full neighborhoodBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\)\.

Frequency of joint\-gap witnesses\.Theorem[1](https://arxiv.org/html/2607.29190#Thmtheorem1)’s geometry is confirmed empirically: sweeping the authored gapδ\\deltaon both real datasets,Pr⁡\[C\]\\Pr\[C\]tracksmin⁡\(δ,ε\)\\min\(\\delta,\\varepsilon\)\(correlation1\.01\.0/0\.960\.96; Table S44\)\. Joint\-gap witnesses follow the geometry of a provenance\-shifted threshold and arise in every setting we measured, at3\.53\.5–12%12\\%natural within\-setting frequency \(Table[7](https://arxiv.org/html/2607.29190#S6.T7)\); DevOps is boundary\-constructed \(Table S9\)\. OPA and GoRules ZEN\(GoRules[2024](https://arxiv.org/html/2607.29190#bib.bib23)\)reproduce the analytic taxonomy exactly \(agreement1\.0001\.000; Table S24\) and Marble\(Checkmarble[2024](https://arxiv.org/html/2607.29190#bib.bib46)\)yieldsCC\-set Jaccard1\.0001\.000\(Table S21\), and a second real adapter reproduces the taxonomy through Kyverno admission \(Table S23\), ruling out an oracle artifact\.

Point and marginal certificates fail\.Neither pointwise exactness nor channel\-wise composition suffices: on the witness setW=\{clean\-safe\}∖RW=\\\{\\text\{clean\-safe\}\\\}\\setminus R, which any sound gate must refuse \(Proposition[3](https://arxiv.org/html/2607.29190#Thmproposition3)\), the exact OPA predicate allows*all*witnesses, and every other point\-evaluating gate \(learned, LLM judges, guard model\(Inanet al\.[2023](https://arxiv.org/html/2607.29190#bib.bib34)\)\) behaves the same, while every neighborhood\-evaluating gate refusesWWwithCFA=0\\mathrm\{CFA\}=0\(Tables[5](https://arxiv.org/html/2607.29190#S6.T5), S17\)\. A stronger3636B\-MoE judge does not close the gap \(≤61%\\leq 61\\%ofWWallowed, unchanged at temperature0\): the results are explained by the evaluation locus: added judge capacity does not provide a neighborhood certificate\. By their published evaluation semantics, deployed enforcers AgentSpec and VeriGuard evaluate only the observed\(z,a\)\(z,a\)and admit every witness by construction \(Table S18\)\.

### 6\.3End\-to\-end agent and system validation

Question\.*Do point and marginal failures produce concrete unsafe effects in a running agent, and does CAGE stop them?* Setup\.Full chains with committed side effects: finance/SRE money\-commit and alert\-suppression episodes, a live k8s/Kyverno cluster on a stale\-registry TOCTOU surface with a real MCP write path, and Marble’s decision API\. Result\.Table[6](https://arxiv.org/html/2607.29190#S6.T6): marginal composition and a transcript classifier with point accuracy1\.001\.00commit at the full no\-gate rate, pre\-execution screening at0\.44/0\.230\.44/0\.23\(Table S19\); only the joint certificate and the oracle commit none on every substrate, safe controls non\-vacuous\. CaMeL and the joint certificate are orthogonal: each blocks a case the other admits \(Table S18\)\. Gate overhead is≈10​μ\\approx 10\\,\\mus vs≈2\.5\\approx 2\.5s LLM decode; protocols: Tables S18 \(AgentSpec/VeriGuard/CaMeL\), S20 \(k8s/Kyverno\), S22 \(Marble\)\.

Table 6:End\-to\-end validation on deployed substrates: CAGE blocks the unsafe effect while the matching safe control passes \(✓\\checkmark; the MCP\-write arm has no safe\-control counterpart\)\.
### 6\.4Certificate soundness and autonomy on real settings

Question\.*Is every certified allow oracle\-safe, while the gate still allows a useful fraction of the robust\-safe set?* Setup\.Primary setting: executable policy\-as\-code \(labels from a realopa evalengine\) over real IEEE\-CIS marginals; each Table[7](https://arxiv.org/html/2607.29190#S6.T7)row carries its backend tag\.

Table 7:Soundness and robust\-safe autonomy across the evaluated settings atd=1d\{=\}1,ε=0\.10\\varepsilon\{=\}0\.10: every certified allow is oracle\-safe \(Callow=Uallow=CFA=0C\_\{\\mathrm\{allow\}\}\{=\}U\_\{\\mathrm\{allow\}\}\{=\}\\mathrm\{CFA\}\{=\}0\) withRallow\>0R\_\{\\mathrm\{allow\}\}\>0throughout; zeros carry Wilson\-95% upper bounds \(Table S51\)\. Per\-setting sources: Tables S27 \(OpenFisca\), S3 \(OPA\), S1 \(IEEE\-CIS\), S2 \(NAB\), S9 \(PSD2/AML\)\.In Table[7](https://arxiv.org/html/2607.29190#S6.T7), CFA measures soundness, whereasRallowR\_\{\\mathrm\{allow\}\}measures the fraction of robust\-safe decisions retained for autonomous execution\.

Result: soundness without vacuity\.Across Table[7](https://arxiv.org/html/2607.29190#S6.T7), every certified allow is oracle\-safe, while every setting retains nonzero robust\-safe coverage\. On IEEE\-CIS, no fraud is observed in the autonomous tranche, whereas33–4%4\\%of blocked transactions are fraudulent\. This contrast captures the role of abstention: the certificate removes decisions near an unsafe boundary rather than merely improving point accuracy\.

The same pattern holds in three additional settings \(robust\-safe coverage1111–38%38\\%; Table S9\); scaling sweeps reach63%63\\%while uncertified attacks keep9090–98%98\\%false allows \(Table S8\)\. Under known ground truth, CAGE\-Lip recovers65%65\\%of the exact robust\-safe set with zero measured policy false allows\. The corresponding Wilson upper bound is2\.2%2\.2\\%\(Table S7\)\. The nonzero entry for CAGE\-Lip in Table[5](https://arxiv.org/html/2607.29190#S6.T5)results from base\-gate policy misfit; the neighborhood certificate remains valid for the learned gate \(Table S6\)\.

Adaptive attacks and policy shift\.An adaptive adversary knowinggθ,Bd,ε,τ,Safeg\_\{\\theta\},B\_\{d,\\varepsilon\},\\tau,\\operatorname\{Safe\}keeps1\.71\.7–15%15\\%false allows through a point gate \(all search families\); CAGE removes them all \(Table S10\); adaptive display\-channel attacks are likewise removed \(Table S12\)\. Under policy shift only the uncertified component breaks: learned adaptive\-FA reaches47\.5%\\mathbf\{47\.5\\%\}on a held\-out threshold, certified0%0\\%\(Table S11\)\.

Implicit policy: a gate\-fidelity stress test\.With the real IEEE\-CISisFraudlabel as policy \(outside the affine fragment\), only gate\-level certification is available: Lip certifies72%72\\%of safe transactions, RS40%40\\%; under attack a utility\-matched point gate re\-admits≈48%\\approx 48\\%of fraud vs41%/4\.4%41\\%/4\.4\\%certified \(Table S13\)\.

Ablations\.Soundness is invariant on every grid tested \(ε×τ\\varepsilon\\times\\tau,σ\\sigma, engine\-labelled, backend\-swap; Tables S3–S5\); only utility and cost move; the MILP ceiling certifiesRallow=100%R\_\{\\mathrm\{allow\}\}=100\\%, locating the deficit in learned margin \(Table S6\)\.

External validity\.A deployed third\-party rule carries the threshold idiom itself: OpenFisca\-France’s social\-housing income ceilings vary by zone\(OpenFisca Community[2024](https://arxiv.org/html/2607.29190#bib.bib24)\), with gaps of EUR 5,029–34,543; the point gate grants all1,7731\{,\}773joint\-gap witnesses, the exact certificate none \(Table[7](https://arxiv.org/html/2607.29190#S6.T7); Table S27\)\. The same structure is first\-class in DMN decision tables and policy code\(Open Policy Agent Authors[2024a](https://arxiv.org/html/2607.29190#bib.bib19); Microsoft[2024](https://arxiv.org/html/2607.29190#bib.bib22)\), and in the AML engines Tazama\(Tazama Project \(LF Charities\)[2024](https://arxiv.org/html/2607.29190#bib.bib47)\)and Marble\(Checkmarble[2024](https://arxiv.org/html/2607.29190#bib.bib46)\)\(Table S26\)\. The PSD2/AML thresholds\(European Commission[2018](https://arxiv.org/html/2607.29190#bib.bib20); Financial Crimes Enforcement Network \(FinCEN\)[2024](https://arxiv.org/html/2607.29190#bib.bib21)\)instantiate the continuous mechanism with source\-locked constants \(Tables S9, S24\)\. What remains unmeasured is prevalence in deployed agentic pipelines: three protocol\-frozen scans and a registry adjudication return pipeline\-provenance nulls \(0/310/31documentedθ​\(s\)\\theta\(s\); Tables S24, S25\)\. We therefore claim existence, realizability, and mechanism; field prevalence remains unmeasured\. With four real proposers \(three Qwen2\.5 variants and the 36B\-MoEqwen3\.6\), the measured certified false\-allow rate remains zero for every proposer and domain \(Tables S14–S16\)\.

Takeaway\.In the implicit\-policy setting, performance is evaluated relative to the soundness limit of Proposition[3](https://arxiv.org/html/2607.29190#Thmproposition3)\. At37%37\\%certified autonomy on IEEE\-CIS, in\-budget fraud in the autonomous tranche is4\.4%4\.4\\%, versus53\.2%53\.2\\%for a volume\-matched point gate \(Table S49\)\. On natural traffic, CAGE\-Exact autonomously clears57%57\\%and46%46\\%of IEEE\-CIS and NAB decisions, respectively, whereas the stricter learned backends clear22–14%14\\%\(Table S50\)\.

![Refer to caption](https://arxiv.org/html/2607.29190v1/x4.png)Figure 4:Freshness governs the residual\.*Top:*same\-entity wall\-clockεemp​@​p95\\varepsilon\_\{\\mathrm\{emp\}\}@\\text\{p95\}crosses the declaredε=0\.10\\varepsilon=0\.10\(dashed\) at≈10\\approx 10s staleness \(Table S35\)\.*Bottom:*the system false\-allow grows as the SLA relaxes while certified false\-allow stays0: residual risk is bounded by the measured escape\.
### 6\.5Assumptions and residual risk

Question\.*Does the declared budget\(d=1,ε=0\.10\)\(d\{=\}1,\\varepsilon\{=\}0\.10\)match how real return corruption behaves, and what escapes it?* Setup\.The budget is an empirical claim about return\-assembly failure: seven adapter faults give per\-fault\(d,ε\)\(d,\\varepsilon\), replayed timestamps test freshness, leave\-one\-out on𝒩d\\mathcal\{N\}\_\{d\}tests coverage, and constructor corruption probes the TCB\. Result\.Table[8](https://arxiv.org/html/2607.29190#S6.T8): every fault the budget claims to cover is atomic \(d=1d=1\) with residual insideε=0\.10\\varepsilon=0\.10; the two uncovered faults have no discrete footprint and blow pastε\\varepsilon\(validation\-stack failures\); corrupting the trusted constructor raises verified\-point false\-allow to1\.7%1\.7\\%\(Table S34\); recalibration through a real adapter into Marble holds held\-out, leaking only outside the ball \(Tables S33, S39\)\.

Table 8:Budget measurement from the injected adapter\-fault mechanisms \(40004000/fault; catalogue in Appendix C\)\. Covered faults are atomic \(Pr⁡\[d=1\]=1\.000\\Pr\[d\{=\}1\]=1\.000\) and the validated residual isεemp​@​p95≈0\.079\\varepsilon\_\{\\mathrm\{emp\}\}@\\mathrm\{p95\}\\approx 0\.079–0\.0950\.095\(per\-fault: Table S31\); leave\-one\-out escape is0for every covered class; compound faults land atd≤2d\\leq 2, still sound, a rare triple atd=3d=3\(Table S28\); branch over\-declaration in Table S30\.Freshness is the binding precondition\.Same\-card staleness crossesε\\varepsilonat≈10\\approx 10s; the system false\-allow grows1\.8%→7\.1%1\.8\\%\\to 7\.1\\%with the SLA whileCFA=0\\mathrm\{CFA\}=0, soPr⁡\[system false\-allow\]≤Pr⁡\[escape\]\\Pr\[\\text\{system false\-allow\}\]\\leq\\Pr\[\\text\{escape\}\]\(Figure[4](https://arxiv.org/html/2607.29190#S6.F4); Tables S35–S36\); no well\-covered sub\-minute SLA meets<1%<1\\%: recompute*in\-loop*\. Takeaway: a deployment recipe\.Inject the stack’s adapter faults to measure\(d,εemp\)\(d,\\varepsilon\_\{\\mathrm\{emp\}\}\); declare𝒩d\\mathcal\{N\}\_\{d\}, verify leave\-one\-out escape0; set per\-fieldε\\varepsilonand the SLA soεemp​@​p95≤ε\\varepsilon\_\{\\mathrm\{emp\}\}@\\text\{p95\}\\leq\\varepsilon\(Tables S37–S38\); audit certified allows; refuse deployment on failed Table[2](https://arxiv.org/html/2607.29190#S5.T2)diagnostics\.

Dimension and cost\.The regime is low\-dimensional typed returns, sound throughk=50k=50; above it we project onto the typed policy state \(Tables S46, S40\)\. Certified cost: exact<1​μ<1\\,\\mus, Lip77–1717ms, RS1010–132132ms \(1\.11\.1–6\.5%6\.5\\%of decode; Tables S6, S42\); per\-field budgets and extensions: Tables S29/S38/S47\.

## 7Discussion, Scope, and Limitations

CAGE formulates authorization over typed tool returns as a joint\-neighborhood decision\. The non\-composition result identifies pairs that are safe under each marginal check yet unsafe under a combined binding and numerical deviation\. Across policy\-engine, regulatory, and real\-transaction settings, the joint certificates remove measured in\-budget policy false allows while retaining useful autonomy; CAGE\-Exact is policy\-certified on the verified fragment, CAGE\-Lip and CAGE\-RS extend it to learned gates under an explicit gate–policy fidelity condition\.

The guarantee applies to a single authorization decision and assumes a validated typed\-return constructor, complete mediation, an enumerable discrete neighborhood, and continuous uncertainty within the calibrated freshness and numerical budget; budget\-escape \(1\.8%→7\.1%1\.8\\%\\to 7\.1\\%, Figure[4](https://arxiv.org/html/2607.29190#S6.F4)\) and constructor\-corruption \(0→1\.7%0\\to 1\.7\\%\) measurements quantify what happens when these conditions weaken\. Cross\-turn accumulation, tool selection, prompt\-injection resistance, MCP metadata, and multi\-step execution remain uncertified; boundary\-seeking traffic can inflate abstention but never converts it into a false allow \(Table S41\); learned backends require continued gate–policy auditing \(false\-allow≤0\.021\\leq 0\.021at95%95\\%; Table S43\)\.

The results support joint\-neighborhood authorization as a runtime control wherever typed\-return uncertainty can be measured and enforced\. Further work should measure provenance\-conditioned policies and binding faults in the field, extend the certificate to sequential decisions, and tie calibration to live validation infrastructure\. CAGE therefore provides a calibrated authorization mechanism for decisions whose safety depends on uncertain typed returns\.

## References

- M\. Alshiekh, R\. Bloem, R\. Ehlers, B\. Könighofer, S\. Niekum, and U\. Topcu \(2018\)Safe reinforcement learning via shielding\.InProc\. 32nd AAAI Conference on Artificial Intelligence,Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- C\. Anil, J\. Lucas, and R\. Grosse \(2019\)Sorting out Lipschitz function approximation\.InProceedings of the 36th International Conference on Machine Learning \(ICML\),Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px1.p1.7)\.
- Anthropic \(2024\)Model context protocol specification\.Note:https://modelcontextprotocol\.io/specificationOpen protocol for connecting agents to external tools and data sources\.Cited by:[Appendix B](https://arxiv.org/html/2607.29190#A2.SS0.SSS0.Px1.p1.2)\.
- A\. Ben\-Tal, L\. El Ghaoui, and A\. Nemirovski \(2009\)Robust optimization\.Princeton University Press\.Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- T\. Boissin, F\. Mamalet, T\. Fel, A\. M\. Picard, T\. Massena, and M\. Serrurier \(2025\)An adaptive orthogonal convolution scheme for efficient and flexible CNN architectures\.Proceedings of the 42nd International Conference on Machine Learning \(ICML 2025\), PMLR 267\.Cited by:[§5\.1](https://arxiv.org/html/2607.29190#S5.SS1.p1.8)\.
- A\. Bojchevski, J\. Gasteiger, and S\. Günnemann \(2020\)Efficient robustness certificates for discrete data: sparsity\-aware randomized smoothing for graphs, images and more\.InProc\. 37th International Conference on Machine Learning,Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px1.p1.7)\.
- Checkmarble \(2024\)Marble: open\-source real\-time fraud and AML decision engine\.Note:https://github\.com/checkmarble/marbleVersion 1\.4\.0 used in this work\.Cited by:[§6\.2](https://arxiv.org/html/2607.29190#S6.SS2.p3.10),[§6\.4](https://arxiv.org/html/2607.29190#S6.SS4.p8.3)\.
- S\. Chen, J\. Piet, C\. Sitawarin, and D\. Wagner \(2025\)StruQ: defending against prompt injection with structured queries\.In34th USENIX Security Symposium \(USENIX Security 25\),Seattle, WA,pp\. 2383–2400\.Note:Separates prompt and data into two channels\.External Links:[Link](https://www.usenix.org/conference/usenixsecurity25/presentation/chen-sizhe)Cited by:[§1](https://arxiv.org/html/2607.29190#S1.p1.1)\.
- J\. M\. Cohen, E\. Rosenfeld, and J\. Z\. Kolter \(2019\)Certified adversarial robustness via randomized smoothing\.InProceedings of the 36th International Conference on Machine Learning \(ICML 2019\),PMLR, Vol\.97,pp\. 1310–1320\.Note:Model\-agnosticℓ2\\ell\_\{2\}robustness certificate via Gaussian smoothing\.External Links:1902\.02918Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px1.p1.7)\.
- D\. Das, L\. Beurer\-Kellner, M\. Fischer, and M\. Baader \(2025\)CommandSans: securing AI agents with surgical precision prompt sanitization\.arXiv preprint arXiv:2510\.08829\.Note:Token\-level non\-blocking instruction sanitization\.External Links:2510\.08829Cited by:[§1](https://arxiv.org/html/2607.29190#S1.p1.1)\.
- E\. Debenedetti, I\. Shumailov, T\. Fan, J\. Hayes, N\. Carlini, D\. Fabian, C\. Kern, C\. Shi, A\. Terzis, and F\. Tramèr \(2025\)Defeating prompt injections by design\.arXiv preprint arXiv:2503\.18813\.Note:CaMeL: capability\-based control\- and data\-flow defense\.External Links:2503\.18813Cited by:[Table S18](https://arxiv.org/html/2607.29190#A5.T18),[§1](https://arxiv.org/html/2607.29190#S1.p1.1)\.
- E\. Debenedetti, J\. Zhang, M\. Balunović, L\. Beurer\-Kellner, M\. Fischer, and F\. Tramèr \(2024\)AgentDojo: a dynamic environment to evaluate prompt injection attacks and defenses for LLM agents\.InAdvances in Neural Information Processing Systems 37 \(NeurIPS 2024\), Datasets and Benchmarks Track,External Links:2406\.13352,[Link](https://agentdojo.spylab.ai/)Cited by:[Appendix B](https://arxiv.org/html/2607.29190#A2.SS0.SSS0.Px2.p1.1),[§2](https://arxiv.org/html/2607.29190#S2.p1.1)\.
- European Commission \(2018\)Commission delegated regulation \(eu\) 2018/389: regulatory technical standards for strong customer authentication\.Note:Official Journal of the European Union L 69/23PSD2 RTS: low\-value \(Art\. 16\), contactless \(Art\. 11\), and transaction\-risk\-analysis exemption thresholds \(Art\. 18\)\.Cited by:[§6\.4](https://arxiv.org/html/2607.29190#S6.SS4.p8.3)\.
- Financial Crimes Enforcement Network \(FinCEN\) \(2024\)Currency transaction reporting\.Note:31 CFR 1010\.311AML currency\-transaction\-report hard threshold of $10,000\.Cited by:[§6\.4](https://arxiv.org/html/2607.29190#S6.SS4.p8.3)\.
- K\. Fisler, S\. Krishnamurthi, L\. A\. Meyerovich, and M\. C\. Tschantz \(2005\)Verification and change\-impact analysis of access\-control policies\.InProc\. 27th International Conference on Software Engineering \(ICSE\),Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- M\. Ghitu and M\. Wicker \(2026\)Towards poisoning robustness certification for natural language generation\.arXiv preprint arXiv:2602\.09757\.Note:Targeted Partition Aggregation; certifies tool\-calling validity under training\-set poisoning \(not runtime corruption\)\.Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- GoRules \(2024\)ZEN engine: open\-source business rules engine\.Note:https://gorules\.ioRust\-core JDM decision\-table engine used in fintech; second production engine used to engine\-labelCC\-witnesses\.Cited by:[§6\.2](https://arxiv.org/html/2607.29190#S6.SS2.p3.10)\.
- K\. Greshake, S\. Abdelnabi, S\. Mishra, C\. Endres, T\. Holz, and M\. Fritz \(2023\)Not what you’ve signed up for: compromising real\-world LLM\-integrated applications with indirect prompt injection\.InProceedings of the 16th ACM Workshop on Artificial Intelligence and Security \(AISec ’23\),Note:Coined “indirect prompt injection”\.External Links:[Document](https://dx.doi.org/10.1145/3605764.3623985),2302\.12173Cited by:[Appendix B](https://arxiv.org/html/2607.29190#A2.SS0.SSS0.Px2.p1.1),[§1](https://arxiv.org/html/2607.29190#S1.p1.1),[§2](https://arxiv.org/html/2607.29190#S2.p1.1)\.
- K\. Hines, G\. Lopez, M\. Hall, F\. Zarfati, Y\. Zunger, and E\. Kiciman \(2024\)Defending against indirect prompt injection attacks with spotlighting\.arXiv preprint arXiv:2403\.14720\.Note:Provenance marking for untrusted inputs\.External Links:2403\.14720Cited by:[§1](https://arxiv.org/html/2607.29190#S1.p1.1)\.
- V\. C\. Hu, D\. Ferraiolo, R\. Kuhn, A\. Schnitzer, K\. Sandlin, R\. Miller, and K\. Scarfone \(2014\)Guide to attribute based access control \(ABAC\) definition and considerations\.Technical reportTechnical ReportNIST SP 800\-162,National Institute of Standards and Technology\.Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- P\. Huang, R\. Stanforth, J\. Welbl, C\. Dyer, D\. Yogatama, S\. Gowal, K\. Dvijotham, and P\. Kohli \(2019\)Achieving verified robustness to symbol substitutions via interval bound propagation\.InProc\. 2019 Conference on Empirical Methods in Natural Language Processing,Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px1.p1.7)\.
- H\. Inan, K\. Upasani, J\. Chi, R\. Rungta, K\. Iyer, Y\. Mao, M\. Tontchev, Q\. Hu, B\. Fuller, D\. Testuggine, and M\. Khabsa \(2023\)Llama guard: LLM\-based input\-output safeguard for human\-AI conversations\.arXiv preprint arXiv:2312\.06674\.Cited by:[Table S17](https://arxiv.org/html/2607.29190#A5.T17),[§6\.2](https://arxiv.org/html/2607.29190#S6.SS2.p4.8)\.
- Z\. Ji, Z\. Li, W\. Jiang, Y\. Gao, and S\. Wang \(2026\)Measuring the permission gate: a stress\-test evaluation of Claude Code’s auto mode\.arXiv preprint arXiv:2604\.04978\.Note:AmPermBench: 128\-prompt DevOps stress test; reports an 81% end\-to\-end false\-negative rate and a Tier\-2 coverage gap on in\-project file edits\.External Links:2604\.04978Cited by:[Appendix B](https://arxiv.org/html/2607.29190#A2.SS0.SSS0.Px3.p1.1),[§1](https://arxiv.org/html/2607.29190#S1.p1.1),[§2](https://arxiv.org/html/2607.29190#S2.p1.1)\.
- R\. Jia, A\. Raghunathan, K\. Göksel, and P\. Liang \(2019\)Certified robustness to adversarial word substitutions\.InProc\. 2019 Conference on Empirical Methods in Natural Language Processing,Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px1.p1.7)\.
- J\. Kim, W\. Choi, and B\. Lee \(2025\)Prompt flow integrity to prevent privilege escalation in LLM agents\.arXiv preprint arXiv:2503\.15547\.Note:Confused\-deputy framing; agent isolation \+ privilege guardrails\.Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- A\. Lavin and S\. Ahmad \(2015\)Evaluating real\-time anomaly detection algorithms – the Numenta anomaly benchmark\.In14th IEEE International Conference on Machine Learning and Applications \(ICMLA\),Cited by:[Table S2](https://arxiv.org/html/2607.29190#A5.T2)\.
- G\. Lee, Y\. Yuan, S\. Chang, and T\. S\. Jaakkola \(2019\)Tight certificates of adversarial robustness for randomly smoothed classifiers\.InAdvances in Neural Information Processing Systems 32,Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px1.p1.7)\.
- P\. Li, X\. Zou, Z\. Wu,et al\.\(2025\)SAFEFLOW: a principled protocol for trustworthy and transactional autonomous agent systems\.arXiv preprint arXiv:2506\.07564\.Note:Multi\-layer information\-flow control \+ transactional execution\.Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- Y\. Ling, S\. Yu, Z\. Chen, and C\. Fang \(2026\)Toward secure LLM agents: threat surfaces, attacks, defenses, and evaluation\.arXiv preprint arXiv:2606\.10749\.Note:SoK over 247 papers on agent security\.Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- J\. Liu, X\. Zhao, X\. Shang, and Z\. Shen \(2026\)Dive into Claude Code: the design space of today’s and future AI agent systems\.arXiv preprint arXiv:2604\.14228\.Note:Source\-level analysis of Claude Code v2\.1\.88; the agent loop is a small fraction of the system, the rest being permission systems, hooks, sandboxing, and tooling\.External Links:2604\.14228,[Link](https://github.com/VILA-Lab/Dive-into-Claude-Code)Cited by:[Appendix B](https://arxiv.org/html/2607.29190#A2.SS0.SSS0.Px1.p1.2),[§1](https://arxiv.org/html/2607.29190#S1.p1.1),[§2](https://arxiv.org/html/2607.29190#S2.p1.1)\.
- Microsoft \(2024\)Azure policy built\-in definitions for Key Vault\.Note:https://learn\.microsoft\.com/azure/key\-vault/policy\-referenceBuilt\-in key\-type/key\-size constraints \(keyType→\\tokeySize\)\.Cited by:[§6\.4](https://arxiv.org/html/2607.29190#S6.SS4.p8.3)\.
- L\. Miculicich, M\. Parmar, H\. Palangi, K\. Dvijotham, M\. Montanari, T\. Pfister, and L\. T\. Le \(2025\)VeriGuard: enhancing LLM agent safety via verified code generation\.arXiv preprint arXiv:2510\.05156\.Note:Offline policy synthesis \+ formal verification; online per\-action runtime monitor\.Cited by:[Table S18](https://arxiv.org/html/2607.29190#A5.T18),[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- Open Policy Agent Authors \(2024a\)Gatekeeper policy library\.Note:https://github\.com/open\-policy\-agent/gatekeeper\-libraryCommunity library of reusable OPA Gatekeeper ConstraintTemplates for Kubernetes admission control\.Cited by:[§6\.4](https://arxiv.org/html/2607.29190#S6.SS4.p8.3)\.
- Open Policy Agent Authors \(2024b\)Open policy agent\.Note:https://www\.openpolicyagent\.orgOPA: general\-purpose policy engine with the Rego policy language; CNCF graduated project\.Cited by:[Table 4](https://arxiv.org/html/2607.29190#S6.T4.5.3.5.2.2)\.
- OpenFisca Community \(2024\)OpenFisca: a versatile microsimulation free software\.Note:https://openfisca\.orgLegislation\-as\-code framework; OpenFisca\-France model scanned for the provenance\-conditioned\-threshold idiom\.Cited by:[§6\.4](https://arxiv.org/html/2607.29190#S6.SS4.p8.3)\.
- Qwen Team \(2024\)Qwen2\.5 technical report\.arXiv preprint arXiv:2412\.15115\.Cited by:[Table S17](https://arxiv.org/html/2607.29190#A5.T17)\.
- Y\. Ruan, H\. Dong, A\. Wang, S\. Pitis, Y\. Zhou, J\. Ba, Y\. Dubois, C\. J\. Maddison, and T\. Hashimoto \(2024\)Identifying the risks of LM agents with an LM\-emulated sandbox\.InInternational Conference on Learning Representations \(ICLR 2024\),Note:ToolEmu: LM\-emulated sandbox \+ automatic safety evaluator\.External Links:2309\.15817,[Link](https://toolemu.com/)Cited by:[§1](https://arxiv.org/html/2607.29190#S1.p1.1)\.
- L\. Schwinn, M\. Ladenburger, T\. Beyer, M\. Mofakhami, G\. Gidel, and S\. Günnemann \(2026\)A coin flip for safety: LLM judges fail to reliably measure adversarial robustness\.arXiv preprint arXiv:2603\.06594\.Note:LLM\-judge accuracy collapses to near\-random under adversarial distribution shift\.Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- V\. Siu, J\. He, K\. Montgomery, Z\. Wang, N\. Gong, C\. Wang, and D\. Song \(2026\)A framework for formalizing LLM agent security\.arXiv preprint arXiv:2603\.19469\.Note:Contextual security via oracle functions \(task/action alignment, source authorization, data isolation\)\.Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- Tazama Project \(LF Charities\) \(2024\)Tazama: open\-source real\-time transaction monitoring\.Note:https://github\.com/tazama\-lfCited by:[§6\.4](https://arxiv.org/html/2607.29190#S6.SS4.p8.3)\.
- V\. Tjeng, K\. Xiao, and R\. Tedrake \(2019\)Evaluating robustness of neural networks with mixed integer programming\.InInternational Conference on Learning Representations \(ICLR\),Cited by:[§5\.1](https://arxiv.org/html/2607.29190#S5.SS1.p2.1)\.
- A\. Trockman and J\. Z\. Kolter \(2021\)Orthogonalizing convolutional layers with the Cayley transform\.InInternational Conference on Learning Representations \(ICLR\),Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px1.p1.7)\.
- Y\. Tsuzuku, I\. Sato, and M\. Sugiyama \(2018\)Lipschitz\-margin training: scalable certification of perturbation invariance for deep neural networks\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px1.p1.7)\.
- E\. Wallace, K\. Xiao, R\. Leike, L\. Weng, J\. Heidecke, and A\. Beutel \(2024\)The instruction hierarchy: training LLMs to prioritize privileged instructions\.arXiv preprint arXiv:2404\.13208\.External Links:2404\.13208Cited by:[§1](https://arxiv.org/html/2607.29190#S1.p1.1)\.
- H\. Wang, C\. M\. Poskitt, and J\. Sun \(2026a\)AgentSpec: customizable runtime enforcement for safe and reliable LLM agents\.InProc\. 48th IEEE/ACM Int\. Conf\. on Software Engineering \(ICSE\),Note:DSL of trigger/predicate/enforcement; no trajectorial analysis\.Cited by:[Table S18](https://arxiv.org/html/2607.29190#A5.T18),[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- Z\. Wang, Y\. Gao, Y\. Wang, S\. Liu, H\. Sun, H\. Cheng, G\. Shi, H\. Du, and X\. Li \(2026b\)MCPTox: a benchmark for tool poisoning on real\-world MCP servers\.InProceedings of the AAAI Conference on Artificial Intelligence \(AAAI 2026\),Note:First benchmark for tool\-description poisoning on live MCP servers\.External Links:2508\.14925Cited by:[Appendix B](https://arxiv.org/html/2607.29190#A2.SS0.SSS0.Px1.p1.2),[Appendix B](https://arxiv.org/html/2607.29190#A2.SS0.SSS0.Px2.p1.1),[§2](https://arxiv.org/html/2607.29190#S2.p1.1)\.
- S\. Yao, J\. Zhao, D\. Yu, N\. Du, I\. Shafran, K\. Narasimhan, and Y\. Cao \(2023\)ReAct: synergizing reasoning and acting in language models\.InInternational Conference on Learning Representations \(ICLR 2023\),Note:Canonical think–act–observe agent loop\.External Links:2210\.03629Cited by:[§1](https://arxiv.org/html/2607.29190#S1.p1.1),[§2](https://arxiv.org/html/2607.29190#S2.p1.1)\.
- J\. Yeon, I\. Chaudhary, and G\. Singh \(2025\)Quantifying distributional robustness of agentic tool\-selection\.arXiv preprint arXiv:2510\.03992v1\.Note:ToolCert: certified lower bounds on tool\-selection accuracy under adversarial tool descriptions\.External Links:2510\.03992v1Cited by:[Appendix B](https://arxiv.org/html/2607.29190#A2.SS0.SSS0.Px2.p1.1),[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px2.p1.4)\.
- S\. H\. Zargarbashi, M\. S\. Akhondzadeh, and A\. Bojchevski \(2025\)One sample is enough to make conformal prediction robust\.InAdvances in Neural Information Processing Systems 38 \(NeurIPS 2025\),Note:Certifies the conformal procedure itself; a single noisy forward pass yields robust prediction sets\.External Links:2506\.16553Cited by:[§2](https://arxiv.org/html/2607.29190#S2.SS0.SSS0.Px1.p1.7)\.
- Q\. Zhan, Z\. Liang, Z\. Ying, and D\. Kang \(2024\)InjecAgent: benchmarking indirect prompt injections in tool\-integrated large language model agents\.InFindings of the Association for Computational Linguistics \(ACL 2024\),Note:1,054 test cases over 17 user tools and 62 attacker tools\.External Links:2403\.02691Cited by:[Appendix B](https://arxiv.org/html/2607.29190#A2.SS0.SSS0.Px2.p1.1),[§2](https://arxiv.org/html/2607.29190#S2.p1.1)\.
- H\. Zhang, T\. Weng, P\. Chen, C\. Hsieh, and L\. Daniel \(2018\)Efficient neural network robustness certification with general activation functions\.InAdvances in Neural Information Processing Systems 31 \(NeurIPS\),Cited by:[§5\.1](https://arxiv.org/html/2607.29190#S5.SS1.p2.1)\.

These appendices contain the deferred proofs \(Appendix A\), extended background \(Appendix B\), the fault\-mechanism catalogue \(Appendix C\), the certification algorithm and experimental setup \(Appendix D\), and the additional result tables S1–S51 \(Appendix E\)\. Proposition and theorem numbering is continuous with the main text: Propositions 1–3 and Theorem 1 are stated in the main text, Propositions 4–7 and Definition 1 here\. Throughout the appendices,zzdenotes the validated observed record, following the shorthand introduced in Section 3\.2; elementsz′∈Bd,ε​\(z\)z^\{\\prime\}\\in B\_\{d,\\varepsilon\}\(z\)represent plausible correctly bound returns\.

## Appendix ADeferred proofs

###### Proof of Proposition 1 \(return dependence\)\.

Any pre\-return authorization rule observes the user request, transcript, and proposed tool call, but not the realized return\. Therefore it must assign the same authorization decision to the two executions that differ only inz0z\_\{0\}versusz1z\_\{1\}\. If it allows, it is wrong onz1z\_\{1\}; if it denies, it is conservative onz0z\_\{0\}\. Hence return\-dependent safety cannot be decided soundly and non\-vacuously before the return is observed\. ∎

###### Proof of Theorem 1 \(non\-composition\)\.

Let the continuous variable be one\-dimensional and lets,s′s,s^\{\\prime\}be two discrete states whose thresholds differ byΔ\>0\\Delta\>0:

Safe⁡\(\(s,x\),a\)\\displaystyle\\operatorname\{Safe\}\(\(s,x\),a\)=𝟏​\[x≤q\],\\displaystyle=\\mathbf\{1\}\[x\\leq q\],Safe⁡\(\(s′,x\),a\)\\displaystyle\\operatorname\{Safe\}\(\(s^\{\\prime\},x\),a\)=𝟏​\[x≤q−Δ\]\.\\displaystyle=\\mathbf\{1\}\[x\\leq q\-\\Delta\]\.Continuous\-only safety atss, over the symmetricε\\varepsilon\-ball, requiresx\+ε≤qx\+\\varepsilon\\leq q, i\.e\.x≤q−εx\\leq q\-\\varepsilon\. Discrete\-only safety at the observedxxrequiresx≤q−Δx\\leq q\-\\Delta\. But a joint move is unsafe wheneverx\+ε\>q−Δx\+\\varepsilon\>q\-\\Delta, i\.e\.x\>q−Δ−εx\>q\-\\Delta\-\\varepsilon\. All three conditions hold simultaneously exactly for

x∈\(q−Δ−ε,min⁡\(q−ε,q−Δ\)\],x\\in\\big\(\\,q\-\\Delta\-\\varepsilon,\\ \\min\(q\-\\varepsilon,\\,q\-\\Delta\)\\,\\big\],a nonempty interval of lengthmin⁡\(Δ,ε\)\\min\(\\Delta,\\varepsilon\)\. Any suchxxis a joint\-gap witness: safe under every continuous\-only perturbation atssand under the discrete swap at the observedxx, yet unsafe under the joint perturbations→s′s\\to s^\{\\prime\},x→x\+εx\\to x\+\\varepsilon\. ∎

###### Proof of Proposition 2 \(Lipschitz\-margin certificate\)\.

Fix a branchs′∈𝒩d​\(s\)s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)and anyx′x^\{\\prime\}with‖x′−x‖2≤ε\\\|x^\{\\prime\}\-x\\\|\_\{2\}\\leq\\varepsilon\. ByLcertL\_\{\\mathrm\{cert\}\}\-Lipschitzness ofhθh\_\{\\theta\}in the continuous channel,

hθ​\(s′,x′,a\)\\displaystyle h\_\{\\theta\}\(s^\{\\prime\},x^\{\\prime\},a\)≥hθ​\(s′,x,a\)−Lcert​‖x′−x‖2\\displaystyle\\geq h\_\{\\theta\}\(s^\{\\prime\},x,a\)\-L\_\{\\mathrm\{cert\}\}\\\|x^\{\\prime\}\-x\\\|\_\{2\}≥hθ​\(s′,x,a\)−Lcert​ε\.\\displaystyle\\geq h\_\{\\theta\}\(s^\{\\prime\},x,a\)\-L\_\{\\mathrm\{cert\}\}\\varepsilon\.IfAllowLip⁡\(z,a\)=1\\operatorname\{Allow\}\_\{\\mathrm\{Lip\}\}\(z,a\)=1thenhθ​\(s′,x,a\)≥mins′′∈𝒩d​\(s\)⁡hθ​\(s′′,x,a\)\>Lcert​εh\_\{\\theta\}\(s^\{\\prime\},x,a\)\\geq\\min\_\{s^\{\\prime\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)\}h\_\{\\theta\}\(s^\{\\prime\\prime\},x,a\)\>L\_\{\\mathrm\{cert\}\}\\varepsilon, sohθ​\(s′,x′,a\)\>0h\_\{\\theta\}\(s^\{\\prime\},x^\{\\prime\},a\)\>0\. As\(s′,x′\)\(s^\{\\prime\},x^\{\\prime\}\)ranges overBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\), the learned gate stays on the allow side throughout\. ∎

###### Proof of Proposition 3 \(soundness requires boundary abstention\)\.

Supposem​\(z,a\)<εm\(z,a\)<\\varepsilon\. ThenBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\)contains a pointz′=\(s′,x′\)z^\{\\prime\}=\(s^\{\\prime\},x^\{\\prime\}\)withSafe⁡\(z′,a\)=0\\operatorname\{Safe\}\(z^\{\\prime\},a\)=0, and soundness forcesAllow⁡\(z,a\)=0\\operatorname\{Allow\}\(z,a\)=0; contrapositivelyAllow⁡\(z,a\)=1\\operatorname\{Allow\}\(z,a\)=1forcesm​\(z,a\)≥εm\(z,a\)\\geq\\varepsilon, with no assumption on the unsafe set\. When the unsafe set is closed the infimum definingmmis attained, so the same argument applies atm=εm=\\varepsilonand the implication sharpens tom​\(z,a\)\>εm\(z,a\)\>\\varepsilon\. HencePr⁡\[Allow=1\]≤Pr⁡\[m≥ε\]\\Pr\[\\operatorname\{Allow\}=1\]\\leq\\Pr\[m\\geq\\varepsilon\]; the oracle robust gate allows exactlyR=\{m\>ε\}R=\\\{m\>\\varepsilon\\\}, andPr⁡\[m≥ε\]=Pr⁡\[m\>ε\]\\Pr\[m\\geq\\varepsilon\]=\\Pr\[m\>\\varepsilon\]whenever the boundary\{m=ε\}\\\{m=\\varepsilon\\\}has measure zero \(true of our continuous marginals\), giving equality\. A joint\-gap witness contains an unsafe point insideBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\)by definition and is therefore refused, again with no closedness assumption\. ∎

###### Proposition 4\(Exactness of enumeration\)\.

Fix\(z,a\)\(z,a\)withz=\(s,x\)z=\(s,x\)and𝒩d​\(s\)\\mathcal\{N\}\_\{d\}\(s\)finite\. If each per\-branch boundp¯​\(s′,x,a\)\\underline\{p\}\(s^\{\\prime\},x,a\)is a valid lower confidence bound oninf‖x′−x‖2≤εpθ​\(s′,x′,a\)\\inf\_\{\\\|x^\{\\prime\}\-x\\\|\_\{2\}\\leq\\varepsilon\}p\_\{\\theta\}\(s^\{\\prime\},x^\{\\prime\},a\)at level1−αbranch1\-\\alpha\_\{\\mathrm\{branch\}\}withαbranch=αFWER/\|𝒩d​\(s\)\|\\alpha\_\{\\mathrm\{branch\}\}=\\alpha\_\{\\mathrm\{FWER\}\}/\|\\mathcal\{N\}\_\{d\}\(s\)\|, then with probability at least1−αFWER1\-\\alpha\_\{\\mathrm\{FWER\}\},p¯joint​\(s,x,a\)≤infz′∈Bd,ε​\(z\)pθ​\(z′,a\)\\underline\{p\}\_\{\\mathrm\{joint\}\}\(s,x,a\)\\leq\\inf\_\{z^\{\\prime\}\\in B\_\{d,\\varepsilon\}\(z\)\}p\_\{\\theta\}\(z^\{\\prime\},a\), and the discrete minimization contributes no Monte\-Carlo error\.

###### Proof of Proposition[4](https://arxiv.org/html/2607.29190#Thmproposition4)\.

By assumption each eventEs′=\{p¯​\(s′,x,a\)≤inf‖x′−x‖2≤εpθ​\(s′,x′,a\)\}E\_\{s^\{\\prime\}\}=\\\{\\underline\{p\}\(s^\{\\prime\},x,a\)\\leq\\inf\_\{\\\|x^\{\\prime\}\-x\\\|\_\{2\}\\leq\\varepsilon\}p\_\{\\theta\}\(s^\{\\prime\},x^\{\\prime\},a\)\\\}holds with probability at least1−αbranch1\-\\alpha\_\{\\mathrm\{branch\}\}withαbranch=αFWER/\|𝒩d​\(s\)\|\\alpha\_\{\\mathrm\{branch\}\}=\\alpha\_\{\\mathrm\{FWER\}\}/\|\\mathcal\{N\}\_\{d\}\(s\)\|\. A union bound over the finitely many branches givesPr⁡\[⋂s′∈𝒩d​\(s\)Es′\]≥1−αFWER\\Pr\[\\bigcap\_\{s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)\}E\_\{s^\{\\prime\}\}\]\\geq 1\-\\alpha\_\{\\mathrm\{FWER\}\}\. On that event,

p¯joint​\(s,x,a\)=mins′∈𝒩d​\(s\)⁡p¯​\(s′,x,a\)≤mins′∈𝒩d​\(s\)​inf‖x′−x‖2≤εpθ​\(s′,x′,a\)=infz′∈Bd,ε​\(z\)pθ​\(z′,a\),\\underline\{p\}\_\{\\mathrm\{joint\}\}\(s,x,a\)=\\min\_\{s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)\}\\underline\{p\}\(s^\{\\prime\},x,a\)\\\\ \\leq\\min\_\{s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)\}\\inf\_\{\\\|x^\{\\prime\}\-x\\\|\_\{2\}\\leq\\varepsilon\}p\_\{\\theta\}\(s^\{\\prime\},x^\{\\prime\},a\)=\\inf\_\{z^\{\\prime\}\\in B\_\{d,\\varepsilon\}\(z\)\}p\_\{\\theta\}\(z^\{\\prime\},a\),where the last equality holds becauseBd,ε​\(z\)=⋃s′∈𝒩d​\(s\)\{s′\}×\{x′:‖x′−x‖2≤ε\}B\_\{d,\\varepsilon\}\(z\)=\\bigcup\_\{s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)\}\\\{s^\{\\prime\}\\\}\\times\\\{x^\{\\prime\}:\\\|x^\{\\prime\}\-x\\\|\_\{2\}\\leq\\varepsilon\\\}\. The outer minimum is taken over the finite, exactly enumerated set𝒩d​\(s\)\\mathcal\{N\}\_\{d\}\(s\), so it adds no sampling error beyond the per\-branch continuous estimates\. ∎

###### Proposition 5\(Smoothing buffer and approach to the floor\)\.

Suppose on each branchs′∈𝒩d​\(s\)s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)the base gate realizes the oracle as a halfspace,pθ​\(s′,x,a\)=Φ​\(ms′​\(x\)/σ\)p\_\{\\theta\}\(s^\{\\prime\},x,a\)=\\Phi\(m\_\{s^\{\\prime\}\}\(x\)/\\sigma\)withms′m\_\{s^\{\\prime\}\}the signed distance to that branch’s boundary\. Then in the Monte\-Carlo–exact limit the certified gate allows\(z,a\)\(z,a\)iffm​\(z,a\)≥ε\+σ​Φ−1​\(τ\)m\(z,a\)\\geq\\varepsilon\+\\sigma\\Phi^\{\-1\}\(\\tau\); forτ\>12\\tau\>\\tfrac\{1\}\{2\}the allow region is contained in\{m\>ε\}\\\{m\>\\varepsilon\\\}and converges to it asσ​Φ−1​\(τ\)→0\\sigma\\Phi^\{\-1\}\(\\tau\)\\to 0\.

###### Proof of Proposition[5](https://arxiv.org/html/2607.29190#Thmproposition5)\.

In the Monte\-Carlo–exact limit the lower confidence bound equalspθp\_\{\\theta\}, so the per\-branch certified bound isp¯​\(s′,x,a\)=Φ​\(Φ−1​\(pθ​\(s′,x,a\)\)−ε/σ\)\\underline\{p\}\(s^\{\\prime\},x,a\)=\\Phi\\\!\\bigl\(\\Phi^\{\-1\}\(p\_\{\\theta\}\(s^\{\\prime\},x,a\)\)\-\\varepsilon/\\sigma\\bigr\)and the gate allows iffmins′∈𝒩d​\(s\)⁡p¯​\(s′,x,a\)≥τ\\min\_\{s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)\}\\underline\{p\}\(s^\{\\prime\},x,a\)\\geq\\tau\. Substitutingpθ​\(s′,x,a\)=Φ​\(ms′​\(x\)/σ\)p\_\{\\theta\}\(s^\{\\prime\},x,a\)=\\Phi\(m\_\{s^\{\\prime\}\}\(x\)/\\sigma\),

p¯​\(s′,x,a\)≥τ\\displaystyle\\underline\{p\}\(s^\{\\prime\},x,a\)\\geq\\tau⇔ms′​\(x\)σ−εσ≥Φ−1​\(τ\)\\displaystyle\\iff\\tfrac\{m\_\{s^\{\\prime\}\}\(x\)\}\{\\sigma\}\-\\tfrac\{\\varepsilon\}\{\\sigma\}\\geq\\Phi^\{\-1\}\(\\tau\)⇔ms′​\(x\)≥ε\+σ​Φ−1​\(τ\)\.\\displaystyle\\iff m\_\{s^\{\\prime\}\}\(x\)\\geq\\varepsilon\+\\sigma\\Phi^\{\-1\}\(\\tau\)\.Taking the minimum over branches, the joint rule allows iffm​\(z,a\)=mins′⁡ms′​\(x\)≥ε\+σ​Φ−1​\(τ\)m\(z,a\)=\\min\_\{s^\{\\prime\}\}m\_\{s^\{\\prime\}\}\(x\)\\geq\\varepsilon\+\\sigma\\Phi^\{\-1\}\(\\tau\)\. SinceΦ−1​\(τ\)\>0\\Phi^\{\-1\}\(\\tau\)\>0forτ\>12\\tau\>\\tfrac\{1\}\{2\}\(our deployedτ=0\.90\\tau=0\.90\), the allow region is then contained in\{m\>ε\}\\\{m\>\\varepsilon\\\}and increases to it asσ​Φ−1​\(τ\)→0\\sigma\\Phi^\{\-1\}\(\\tau\)\\to 0; atτ=12\\tau=\\tfrac\{1\}\{2\}the containment weakens to\{m≥ε\}\\\{m\\geq\\varepsilon\\\}\. ∎

###### Proposition 6\(Lipschitz allow region\)\.

WriteLemp≤LcertL\_\{\\mathrm\{emp\}\}\\leq L\_\{\\mathrm\{cert\}\}for the gate’s empirical continuous Lipschitz constant andδmargin​\(x\)=m​\(z,a\)−mins′∈𝒩d​\(s\)⁡hθ​\(s′,x,a\)/Lemp\\delta\_\{\\mathrm\{margin\}\}\(x\)=m\(z,a\)\-\\min\_\{s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)\}h\_\{\\theta\}\(s^\{\\prime\},x,a\)/L\_\{\\mathrm\{emp\}\}for its margin underestimation\. ThenAllowLip⁡\(z,a\)=1\\operatorname\{Allow\}\_\{\\mathrm\{Lip\}\}\(z,a\)=1iff

m​\(z,a\)\>ε\+ε​\(LcertLemp−1\)⏟L​\-slack\+δmargin​\(x\)⏟margin slack\.m\(z,a\)\\ \>\\ \\varepsilon\+\\underbrace\{\\varepsilon\\\!\\left\(\\tfrac\{L\_\{\\mathrm\{cert\}\}\}\{L\_\{\\mathrm\{emp\}\}\}\-1\\right\)\}\_\{L\\text\{\-slack\}\}\+\\underbrace\{\\delta\_\{\\mathrm\{margin\}\}\(x\)\}\_\{\\text\{margin slack\}\}\.

###### Proof of Proposition[6](https://arxiv.org/html/2607.29190#Thmproposition6)\.

By definitionAllowLip⁡\(z,a\)=1\\operatorname\{Allow\}\_\{\\mathrm\{Lip\}\}\(z,a\)=1iffmins′⁡hθ​\(s′,x,a\)\>Lcert​ε\\min\_\{s^\{\\prime\}\}h\_\{\\theta\}\(s^\{\\prime\},x,a\)\>L\_\{\\mathrm\{cert\}\}\\varepsilon, equivalentlymins′⁡hθ​\(s′,x,a\)/Lemp\>\(Lcert/Lemp\)​ε\\min\_\{s^\{\\prime\}\}h\_\{\\theta\}\(s^\{\\prime\},x,a\)/L\_\{\\mathrm\{emp\}\}\>\(L\_\{\\mathrm\{cert\}\}/L\_\{\\mathrm\{emp\}\}\)\\varepsilon\. Substitutingmins′⁡hθ​\(s′,x,a\)/Lemp=m​\(z,a\)−δmargin​\(x\)\\min\_\{s^\{\\prime\}\}h\_\{\\theta\}\(s^\{\\prime\},x,a\)/L\_\{\\mathrm\{emp\}\}=m\(z,a\)\-\\delta\_\{\\mathrm\{margin\}\}\(x\)from the definition ofδmargin\\delta\_\{\\mathrm\{margin\}\}gives

m​\(z,a\)−δmargin​\(x\)\>LcertLemp​ε⇔m​\(z,a\)\>ε​LcertLemp\+δmargin​\(x\)\.m\(z,a\)\-\\delta\_\{\\mathrm\{margin\}\}\(x\)\>\\tfrac\{L\_\{\\mathrm\{cert\}\}\}\{L\_\{\\mathrm\{emp\}\}\}\\varepsilon\\\\ \\iff m\(z,a\)\>\\varepsilon\\tfrac\{L\_\{\\mathrm\{cert\}\}\}\{L\_\{\\mathrm\{emp\}\}\}\+\\delta\_\{\\mathrm\{margin\}\}\(x\)\.Writingε​\(Lcert/Lemp\)=ε\+ε​\(Lcert/Lemp−1\)\\varepsilon\(L\_\{\\mathrm\{cert\}\}/L\_\{\\mathrm\{emp\}\}\)=\\varepsilon\+\\varepsilon\(L\_\{\\mathrm\{cert\}\}/L\_\{\\mathrm\{emp\}\}\-1\)separates the floorε\\varepsilonfrom theLL\-slack; sinceLemp≤LcertL\_\{\\mathrm\{emp\}\}\\leq L\_\{\\mathrm\{cert\}\}theLL\-slack is nonnegative\. When additionallyδmargin​\(x\)≥0\\delta\_\{\\mathrm\{margin\}\}\(x\)\\geq 0\(the gate never overestimates the oracle margin, the fidelity condition measured empirically bycert\_false\_allow\), the allow region is contained in\{m\>ε\}\\\{m\>\\varepsilon\\\}; a gate that overestimates the margin \(δmargin<0\\delta\_\{\\mathrm\{margin\}\}<0\) can allow points withm≤εm\\leq\\varepsilon, which is the empirical fidelity caveat of Table[5](https://arxiv.org/html/2607.29190#S6.T5)\. ∎

###### Definition 1\(Verified affine policy fragment\)\.

A policy is in the*fragment*if, for every actionaaand every discrete states′s^\{\\prime\}in the finite declared vocabulary, its restriction to the continuous fields is a finite conjunction of affine constraints,

Safe⁡\(\(s′,x\),a\)=1⇔⋀j=1mwj​\(s′,a\)⊤​x≤bj​\(s′,a\),\\operatorname\{Safe\}\(\(s^\{\\prime\},x\),a\)=1\\iff\\bigwedge\_\{j=1\}^\{m\}w\_\{j\}\(s^\{\\prime\},a\)^\{\\top\}x\\leq b\_\{j\}\(s^\{\\prime\},a\),with parameters read syntactically from the policy source \(finite categorical branching overs′s^\{\\prime\}; no numeric operations beyond affine comparisons\)\. Membership is decided on the policy’s abstract syntax tree; a policy outside the fragment is reportedunsupportedand routed to the verifier ceiling or a gate\-certified rung, never silently approximated\.

###### Proposition 7\(Exact robust evaluation on the fragment\)\.

For a fragment policy, a branchs′∈𝒩d​\(s\)s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\), and theℓ2\\ell\_\{2\}budgetε\\varepsilon,

∀x′∈Bε​\(x\):Safe⁡\(\(s′,x′\),a\)=1\\displaystyle\\forall x^\{\\prime\}\\in B\_\{\\varepsilon\}\(x\):\\ \\operatorname\{Safe\}\(\(s^\{\\prime\},x^\{\\prime\}\),a\)=1⇔⋀j=1mwj​\(s′,a\)⊤​x\+ε​‖wj​\(s′,a\)‖2≤bj​\(s′,a\)\.\\displaystyle\\iff\\bigwedge\_\{j=1\}^\{m\}w\_\{j\}\(s^\{\\prime\},a\)^\{\\top\}x\+\\varepsilon\\\|w\_\{j\}\(s^\{\\prime\},a\)\\\|\_\{2\}\\leq b\_\{j\}\(s^\{\\prime\},a\)\.ConsequentlyAllowexact⁡\(z,a\)\\operatorname\{Allow\}\_\{\\mathrm\{exact\}\}\(z,a\)is computed exactly inO​\(\|𝒩d​\(s\)\|​m​k\)O\(\|\\mathcal\{N\}\_\{d\}\(s\)\|\\,mk\)arithmetic operations forkkcontinuous fields, and CAGE\-Exact is policy\-certified on the fragment\.

###### Proof\.

For affineg​\(x′\)=w⊤​x′g\(x^\{\\prime\}\)=w^\{\\top\}x^\{\\prime\},sup‖x′−x‖2≤εw⊤​x′=w⊤​x\+ε​‖w‖2\\sup\_\{\\\|x^\{\\prime\}\-x\\\|\_\{2\}\\leq\\varepsilon\}w^\{\\top\}x^\{\\prime\}=w^\{\\top\}x\+\\varepsilon\\\|w\\\|\_\{2\}, attained atx′=x\+ε​w/‖w‖2x^\{\\prime\}=x\+\\varepsilon w/\\\|w\\\|\_\{2\}\(the support function of the ball; a constraint withw=0w=0isxx\-independent\)\. Hence constraintjjholds on the whole ball iffwj⊤​x\+ε​‖wj‖2≤bj​\(s′,a\)w\_\{j\}^\{\\top\}x\+\\varepsilon\\\|w\_\{j\}\\\|\_\{2\}\\leq b\_\{j\}\(s^\{\\prime\},a\), and a finite conjunction holds on the ball iff each conjunct does\. Enumerating the\|𝒩d​\(s\)\|\|\\mathcal\{N\}\_\{d\}\(s\)\|branches and evaluatingmminner products overkkfields gives the stated cost\. Our threshold policies are them=1m\{=\}1, coordinate\-wwcase; the OPA/Rego and JDM suites compile to this fragment, and the sub\-microsecond figure of Table S42 measures exactly this test\. ∎

## Appendix BExtended background

#### Tool\-using agents and harness boundaries\.

An LLM agent runs a think→\\toact\-via\-tool→\\toobserve loop\. The tool has two faces: the executable function \(shell command, HTTP request, SQL query, file edit, payment API, monitoring endpoint\), which can cause side effects, and the representation shown to the model \(name, description, JSON schema\), which can be poisoned, especially when tools are discovered dynamically through protocols such as MCP\(Anthropic[2024](https://arxiv.org/html/2607.29190#bib.bib15); Wanget al\.[2026b](https://arxiv.org/html/2607.29190#bib.bib16)\)\. In Claude Code the model emits structured tool\-use blocks while the harness validates, checks permissions, dispatches tools, optionally sandboxes execution, and stores transcripts\(Liuet al\.[2026](https://arxiv.org/html/2607.29190#bib.bib1)\); the safety layer includes rule\-based permission checks, hooks, an auto\-mode classifier, built\-in and MCP tools, sandboxing, and subagents\. The right object to certify is thus the runtime decision boundary exposed by the harness rather than the raw LLM\.

#### MCP, tool poisoning, and indirect prompt injection\.

Indirect prompt injection differs from direct injection: malicious instructions enter through third\-party content \(emails, web pages, retrieved documents, tool outputs, tool descriptions, or agent\-to\-agent messages\)\(Greshakeet al\.[2023](https://arxiv.org/html/2607.29190#bib.bib5)\), are read by the model, and influence future privileged actions, as quantified by dedicated benchmarks\(Zhanet al\.[2024](https://arxiv.org/html/2607.29190#bib.bib6); Debenedettiet al\.[2024](https://arxiv.org/html/2607.29190#bib.bib7)\)\. MCP\-style discovery expands the surface: an external server may publish tool descriptions that become part of the agent context, so tool\-metadata poisoning is close to RAG poisoning over tool descriptions, with the added consequence that selected tools have real side effects\(Wanget al\.[2026b](https://arxiv.org/html/2607.29190#bib.bib16); Yeonet al\.[2025](https://arxiv.org/html/2607.29190#bib.bib17)\)\. We target a different stage: a tool has already returned a typed object, and the question is whether the agent may act on it\.

#### Permission classifiers and their limits\.

Deployed permission systems are mostly pre\-execution: Claude Code auto mode classifies proposed tool calls into safe, unsafe, or manual\-approval, with a three\-tier structure \(read\-only auto\-allowed, in\-project edits may bypass the classifier, shell/external actions passed to a transcript classifier\), and a stress test reports high false\-negative rates on ambiguous DevOps tasks plus a coverage gap where the same state\-changing effect is reachable through an unevaluated tool path\(Jiet al\.[2026](https://arxiv.org/html/2607.29190#bib.bib2)\)\. Safety thus depends on where the boundary sits as much as on classifier accuracy: a classifier over tool calls does not certify whether a later decision on a returned object is robust\.

## Appendix CFault mechanisms and a worked example

Throughout, the typed constructor, schema validation, and the integrity and freshness checks constitute the*trusted computing base*\(TCB\) assumed by the certificate: the guarantee is conditional on this base, and Section 6\.5 measures what happens as it weakens \(constructor corruption, freshness escape\)\.

The discrete budgetd=1d=1models a single admissible*binding*fault rather than arbitrary string rewriting:s′∈𝒩d​\(s\)s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)may be a stale provenance tag, a schema\-version mismatch, a confused policy pack, a multiplexed return attributed to the wrong tool, or a TOCTOU race between an environment label and the numerical fields\. The continuous budget models bounded distortion of operational quantities that remain subject to range checks, unit normalization, plausibility filters, signed telemetry, or partial integrity checks, so‖x′−x‖2≤ε\\\|x^\{\\prime\}\-x\\\|\_\{2\}\\leq\\varepsiloncaptures the residual uncertainty left after ordinary validation rather than free choice of values\. Section 6\.5 injects seven such faults \(provenance/policy\-pack/TOCTOU swaps, stale cache reads, schema skew, key collisions, numeric jitter, normalization skew\) and measures the induced\(d,ε\)\(d,\\varepsilon\); re\-read jitter \(frac\_in\_B=0\.998\\texttt\{frac\\\_in\\\_B\}=0\.998\) and normalizer skew \(0\.9740\.974\) are covered fully, while the faultsε\\varepsilonmisses \(schema transposition, key collisions\) are exactly those a schema/identity validation layer is meant to catch\. The catalogue measures*single*faults; simultaneous faults in one return\-assembly window are excluded by an explicit fault\-independence assumption \(Section 3\.2\), with the deterministic backend’sd≤3d\\leq 3coverage \(Table[S29](https://arxiv.org/html/2607.29190#A5.T29)\) as the fallback if compounding is realistic in a given stack\.

#### Worked example\.

An infrastructure agent may receive an aggregated deployment return whose discrete partss\(env,namespace,tool\_source,policy\_pack\) and numerical partxx\(cpu\_limit,memory,risk\_score,estimated\_cost\) are produced by ahelm diff→\\topolicy scan→\\tocost estimate→\\torisk score stack\. A low\-integrity adapter or stale cache can confusestaging↔prod\\texttt\{staging\}\\leftrightarrow\\texttt\{prod\}orhelm\_diff↔external\_report\\texttt\{helm\\\_diff\}\\leftrightarrow\\texttt\{external\\\_report\}while the numerical fields stay close because they are normalized, range\-checked, or signed: exactly ad=1d=1provenance swap paired with a within\-ε\\varepsilonnumerical move\. Likewise, a calibrated financial risk score can be numerically plausible yet unsafe under a stricter source \(a sanctions screen rather than a credit check\), so the same value carries different authorization meaning under the swapped provenance\.

## Appendix DAlgorithm and experimental setup

#### Certification algorithm\.

Every rung shares the discrete step: given a typed return\(s,x\)\(s,x\), a candidate actionaa, and budgets\(d,ε\)\(d,\\varepsilon\), compute𝒩d​\(s\)=\{s′:Ddisc​\(s,s′\)≤d\}\\mathcal\{N\}\_\{d\}\(s\)=\\\{s^\{\\prime\}:D\_\{\\mathrm\{disc\}\}\(s,s^\{\\prime\}\)\\leq d\\\}exactly and allow only if every branchs′∈𝒩d​\(s\)s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)passes its continuous test; the branch test depends on the backend\.*CAGE\-Exact \(rung 1\)\.*For a fragment policy \(Definition[1](https://arxiv.org/html/2607.29190#Thmdefinition1)\), test every affine constraint at its ball\-worst point,wj⊤​x\+ε​‖wj‖2≤bj​\(s′,a\)w\_\{j\}^\{\\top\}x\+\\varepsilon\\\|w\_\{j\}\\\|\_\{2\}\\leq b\_\{j\}\(s^\{\\prime\},a\)\(Proposition[7](https://arxiv.org/html/2607.29190#Thmproposition7); differential validation against OPA over200,000200\{,\}000returns: Table S48\); no learned gate, no sampling, and none of\(σ,τ,M\)\(\\sigma,\\tau,M\)\.*CAGE\-Lip \(rung 2\)\.*Test the deterministic marginhθ​\(s′,x,a\)\>Lcert​εh\_\{\\theta\}\(s^\{\\prime\},x,a\)\>L\_\{\\mathrm\{cert\}\}\\varepsilon; no sampling and no confidence parameter \(the guarantee is horizon\-invariant, Table[S47](https://arxiv.org/html/2607.29190#A5.T47)\)\.*CAGE\-RS \(rung 3\)\.*Sampleηj∼𝒩​\(0,σ2​I\)\\eta\_\{j\}\\sim\\mathcal\{N\}\(0,\\sigma^\{2\}I\)\(j=1,…,Mj=1,\\dots,M\), estimate the safe probability ofgθ​\(s′,x\+ηj,a\)g\_\{\\theta\}\(s^\{\\prime\},x\+\\eta\_\{j\},a\), form the Clopper–Pearson lower confidence boundp^LCB​\(s′,x,a\)\\widehat\{p\}\_\{\\mathrm\{LCB\}\}\(s^\{\\prime\},x,a\)at level1−αFWER/\|𝒩d​\(s\)\|1\-\\alpha\_\{\\mathrm\{FWER\}\}/\|\\mathcal\{N\}\_\{d\}\(s\)\|, apply the smoothing boundp¯​\(s′,x,a\)=Φ​\(Φ−1​\(p^LCB\)−ε/σ\)\\underline\{p\}\(s^\{\\prime\},x,a\)=\\Phi\(\\Phi^\{\-1\}\(\\widehat\{p\}\_\{\\mathrm\{LCB\}\}\)\-\\varepsilon/\\sigma\), and allow iffmins′∈𝒩d​\(s\)⁡p¯​\(s′,x,a\)≥τ\\min\_\{s^\{\\prime\}\\in\\mathcal\{N\}\_\{d\}\(s\)\}\\underline\{p\}\(s^\{\\prime\},x,a\)\\geq\\tau\. RS experiments fixσ=0\.10\\sigma=0\.10,τ=0\.90\\tau=0\.90,M=2000M=2000Monte\-Carlo samples per branch \(M=104M=10^\{4\}where stated\), andαFWER=10−3\\alpha\_\{\\mathrm\{FWER\}\}=10^\{\-3\}, unless a sweep varies them explicitly \(Section 6\.1\); the exact and Lipschitz backends use none of these parameters\. The RS confidence guarantees are*per decision*: a deployment over a horizon ofTTdecisions must allocate a lifetime budget across decisions \(e\.g\.,αt=αtotal/T\\alpha\_\{t\}=\\alpha\_\{\\mathrm\{total\}\}/Tor an alpha\-spending schedule\) or fall back to the deterministic Lipschitz rung, whose guarantee carries no sampling confidence term\.

#### Normalization\.

All continuous fields are normalized before training and certification, andε,σ\\varepsilon,\\sigmaare defined in this normalized space: bounded operational quantities are affinely scaled to\[0,1\]\[0,1\], and heavy\-tailed quantities \(amounts, latencies\) are log\-transformed then quantile\- or standard\-deviation\-scaled\. Raw units are used only for display and policy descriptions, soε=0\.10\\varepsilon=0\.10is a radius in normalized operational\-feature space, which is what makes a singleε,σ\\varepsilon,\\sigmameaningful across heterogeneous fields \(risk scores, amounts, latencies, counts, error rates\)\.

#### Computing infrastructure and software\.

All experiments ran on a single workstation running Ubuntu 24\.04 LTS \(Linux kernel 6\.8\), with an Intel Xeon Gold 6326 CPU \(2\.90 GHz\), 495 GiB of RAM, and one NVIDIA RTX PRO 6000 Blackwell GPU \(96 GB VRAM; driver 595\.58\.03, CUDA 13\.2\)\. The analytic core \(exact certification, the frozen detectors, and the frozen\-protocol scans\) is pure Python 3\.12 standard library and requires no GPU; the learned backends usetorch2\.8\.0 withorthogonium0\.0\.4 for the 1\-Lipschitz gate, plusnumpy2\.4\.2,scipy1\.17\.1,scikit\-learn1\.8\.0, andpandas2\.3\.2\. Policy engines and substrates: OPA 1\.17\.1, the GoRules ZEN engine \(zen\-engine0\.53\.0\), Kyverno on a kind cluster, and the Marble decision API; the LLM proposers are served locally through Ollama, with tagsqwen2\.5:7b\-instruct,qwen2\.5\-coder:7b,qwen2\.5:32b, andqwen3\.6:latest\(the last a 36B mixture\-of\-experts, Q4\_K\_M quantization,≈23\\approx 23GB\)\. All timing figures reported in Section 6 were measured on this machine\. Code, exact run commands, and per\-experiment capability tags will be made publicly available\.

## Appendix EAdditional result tables

These tables support Sections 6\.2–6\.5; the main text keeps one key table per claim and relocates the secondary ones here\. Zero cells across these tables carry explicitn/Nn/Nand Wilson\-95% upper bounds, audited in Table[S51](https://arxiv.org/html/2607.29190#A5.T51)\.

### E\.1Core certificate evaluation

Primary real\-data certificate evaluation, backend study, and controlled scaling diagnostics\.

Question\.Is the joint certificate sound and non\-vacuous on real transaction marginals?Setting\.Real IEEE\-CIS marginals,10,00010\{,\}000records per sampling mode \(boundary\-balanced, natural,CC\-targeted\)\.Result\.Sound in every mode \(Callow=Uallow=cert\_false\_allow=0C\_\{\\mathrm\{allow\}\}=U\_\{\\mathrm\{allow\}\}=\\texttt\{cert\\\_false\\\_allow\}=0\) and non\-vacuous onRR; no fraud among certified allows against a2\.72\.7–3\.8%3\.8\\%base rate \(Table[S1](https://arxiv.org/html/2607.29190#A5.T1)\)\.

Table S1:Joint certificate on real IEEE\-CIS marginals \(Section 6\.4\)\. Sound \(Callow=Uallow=cert\_false\_allow=0C\_\{\\mathrm\{allow\}\}=U\_\{\\mathrm\{allow\}\}=\\texttt\{cert\\\_false\\\_allow\}=0\) and non\-vacuous onRRacross sampling modes; fraud rate all/certified\-allowed/blocked:3\.8/0\.0/4\.1%3\.8/0\.0/4\.1\\%\(boundary\-balanced\),2\.8/0\.0/3\.3%2\.8/0\.0/3\.3\\%\(natural\),2\.7/0\.0/2\.8%2\.7/0\.0/2\.8\\%\(CC\-targeted\);10,00010\{,\}000records per mode\.Question\.Do the phenomenon and the certificate transfer to a second real dataset outside finance?Setting\.NAB CloudWatch CPU telemetry \(≈58\\approx 58k rows\) under a staging/production monitoring policy \(δ=0\.08\\delta=0\.08, real q0\.700\.70base threshold\);n=6000n=6000,33seeds\.Result\.NaturalC=10\.91±2\.01%C=10\.91\\pm 2\.01\\%with600600audited witnesses andnaive\_C\_falseallow=1\.0\\texttt\{naive\\\_C\\\_falseallow\}=1\.0; all three backends are sound, with the numeric\-block scaling held\-out validated \(Table[S2](https://arxiv.org/html/2607.29190#A5.T2)\)\.

Table S2:Second real dataset \(Section 6\.2\): NAB AWS CloudWatch CPU telemetry\(Lavin and Ahmad[2015](https://arxiv.org/html/2607.29190#bib.bib33)\)\(≈58\\approx 58k rows\) under a constructed staging/production monitoring policy \(θ​\(s\)\\theta\(s\)gapδ=0\.08\\delta=0\.08,θbase\\theta\_\{\\mathrm\{base\}\}the real CPU q0\.700\.70quantile\);n=6000n=6000,33seeds,ε=0\.10\\varepsilon=0\.10\. NaturalC=10\.91±2\.01%C=10\.91\\pm 2\.01\\%;600600audited joint\-gap witnesses with zero violations;naive\_C\_falseallow=1\.0\\texttt\{naive\\\_C\\\_falseallow\}=1\.0\. Numeric\-block feature scaling \(fscale=4\\texttt\{fscale\}=4, certified constantfscale⋅Lcert\\texttt\{fscale\}\\cdot L\_\{\\mathrm\{cert\}\}\) resolves the Lipschitz underfit soundly\. The NAB anomaly label is a diagnostic only, never the certification label\. Thefscalechoice is held\-out validated: a stratified selection/eval split selectsfscale∗=6\.0\\texttt\{fscale\}^\{\*\}=6\.0on every seed with evalcert\_false\_allow=0\\texttt\{cert\\\_false\\\_allow\}=0andRallow=1\.0R\_\{\\mathrm\{allow\}\}=1\.0\(no soundness cliff on this grid; sound atd=2d=2as well\)\.Question\.Do the results survive when authorization labels come from a real policy engine instead of the analytic oracle?Setting\.opa evalover authored provenance\-conditioned Rego \(55seeds\), then an operating\-point sweep of2424cells \(33seeds×ε×τ×\\times\\,\\varepsilon\\times\\tau\\timesbackend×\\timesdomain,10,80010\{,\}800records, per\-record FWER correction\)\.Result\.Joint\-gap witnesses arise spontaneously at≈10\\approx 10–12%12\\%, the certified gate is sound with zero seed variance, and every sweep cell is sound \(Tables[S3](https://arxiv.org/html/2607.29190#A5.T3)–[S4](https://arxiv.org/html/2607.29190#A5.T4)\)\.

Table S3:Policy\-as\-code grounding \(Section 6\.4\)\. Authorization labels are produced by a real Open Policy Agent engine over authored provenance\-conditioned Rego \(mean±\\pmstd over 5 seeds,ε=σ=0\.10\\varepsilon=\\sigma=0\.10,τ=0\.90\\tau=0\.90\)\. Joint\-gap witnesses \(categoryCC\) arise spontaneously at≈10\\approx 10–12%12\\%; the certified gate is sound with zero seed variance\.Table S4:OPA operating\-point sweep \(Section 6\.4\)\. Realopa evallabels with a per\-record family\-wise correctionαbranch=αFWER/\|𝒩d​\(s\)\|\\alpha\_\{\\mathrm\{branch\}\}=\\alpha\_\{\\mathrm\{FWER\}\}/\|\\mathcal\{N\}\_\{d\}\(s\)\|;33seeds×ε∈\{0\.05,0\.10\}×τ∈\{0\.90,0\.95\}×\{smoothing, Lipschitz\}×3\\times\\,\\varepsilon\\in\\\{0\.05,0\.10\\\}\\times\\tau\\in\\\{0\.90,0\.95\\\}\\times\\\{\\text\{smoothing, Lipschitz\}\\\}\\times 3domains \(10,80010\{,\}800records\)\. All2424cells are sound \(Callow=Uallow=cert\_false\_allow=0C\_\{\\mathrm\{allow\}\}=U\_\{\\mathrm\{allow\}\}=\\texttt\{cert\\\_false\\\_allow\}=0\) while the uncertified gate’s attack\-false\-allow spans0\.300\.30–0\.470\.47; only utility moves\. A separate6060\-pointε×τ\\varepsilon\\times\\taugrid over the three synthetic domains \(ε∈\{0\.03,…,0\.20\}×τ∈\{0\.80,…,0\.95\}\\varepsilon\\in\\\{0\.03,\\dots,0\.20\\\}\\times\\tau\\in\\\{0\.80,\\dots,0\.95\\\}\) and aσ∈\[0\.05,0\.20\]\\sigma\\in\[0\.05,0\.20\]ablation are likewise sound at every point, with financeRallowR\_\{\\mathrm\{allow\}\}falling0\.68→0\.49→00\.68\\to 0\.49\\to 0as\(ε,τ\)\(\\varepsilon,\\tau\)tightens\. The three cells where smoothing goes vacuous at\(ε,τ\)=\(0\.10,0\.95\)\(\\varepsilon,\\tau\)=\(0\.10,0\.95\)are a utility failure rather than a soundness one; the deterministic Lipschitz backend recoversRallow=0\.36R\_\{\\mathrm\{allow\}\}=0\.36–0\.510\.51there\.Question\.How do the certified backends compare on one fixed task, and how much utility does the learned margin leave unclaimed?Setting\.The same trained OPA\-track gate across7575multi\-seed cells, plus a complete big\-MMMILP verification of the identical gate as ceiling \(33seeds,ε=0\.10\\varepsilon=0\.10\)\.Result\.Every cell is sound; smoothing a bounded\-logitLipGateis structurally near\-vacuous; the complete ceiling certifies the gate itself, locating the utility deficit in the learned margin rather than in the certificate \(Tables[S5](https://arxiv.org/html/2607.29190#A5.T5)–[S6](https://arxiv.org/html/2607.29190#A5.T6)\)\.

Table S5:Backend comparison on the OPA track \(Experiment LIP; Section 6\.4\)\. All7575multi\-seed cells are sound \(Callow=Uallow=cert\_false\_allow=0C\_\{\\mathrm\{allow\}\}=U\_\{\\mathrm\{allow\}\}=\\texttt\{cert\\\_false\\\_allow\}=0\);ε=0\.10\\varepsilon=0\.10deterministic entries are mean over five seeds \(finance/SRE/ops\), others ranges across domains\. Smoothing a bounded\-logitLipGateis structurally near\-vacuous \(Rallow≈0R\_\{\\mathrm\{allow\}\}\\approx 0\) and omitted as a backend–architecture mismatch\. At the strict point the finite\-MC tax is≈0\\approx 0\(the deterministic backend is within seed variance ofM=104M\{=\}10^\{4\}smoothing on two of three domains\) and a certified local gradient bound \(≈0\.98≈Lcert=1\\approx 0\.98\\approx L\_\{\\mathrm\{cert\}\}=1\) leaves no removableLL\-slack: the residual deficit to exact utility is learned\-margin deficiency\. Margin geometry: allowed\-RRpoints sit at mean oracle margin0\.3780\.378, refused\-RRat0\.1890\.189, straddlingε\+σ​Φ−1​\(τ\)=0\.228\\varepsilon\+\\sigma\\Phi^\{\-1\}\(\\tau\)=0\.228\(correlation0\.860\.86\): the smoothed allow region converges to the abstention floor from above \(Proposition 5\)\.Table S6:Complete\-verification ceiling \(Section 5\.1\): the same trained OPA\-track gate certified per branch by big\-MMMILP over‖δ‖2≤ε\\\|\\delta\\\|\_\{2\}\\leq\\varepsilon\(circumscribing outer polytope: complete for the polytope, sound and possibly conservative for the ball\), vs the Lipschitz and smoothing backends;33seeds,ε=0\.10\\varepsilon=0\.10,RallowR\_\{\\mathrm\{allow\}\}as finance/SRE/ops\. CV certifies the gate’s entire robust\-safe set; its0\.00850\.0085oracle false\-allow on ops \(the multivariate rule\) is base\-gate fidelity passed through exactly: completeness w\.r\.t\. the gate is not soundness w\.r\.t\. the policy\. MILP branch;α,β\\alpha,\\beta\-CROWN unavailable in this environment\.Question\.What does certification cost when engine\-exact ground truth is available?Setting\.ROPAR\_\{\\mathrm\{OPA\}\}= the engine\-exact robust\-safe set; boundary\-balanced evaluation,ε=0\.10\\varepsilon=0\.10,d=1d=1,33seeds,800800records/domain\.Result\.Point systems pay a boundary price; the gate\-certified Lipschitz backend holds policy false\-allow at0\(Wilson\-95% upper≤0\.022\\leq 0\.022\) while recovering a substantial fraction ofROPAR\_\{\\mathrm\{OPA\}\}\(Table[S7](https://arxiv.org/html/2607.29190#A5.T7)\)\.

Table S7:Gate–policy fidelity benchmark under known ground truth \(EXP\-CX1; Section 6\.4\)\.ROPAR\_\{\\mathrm\{OPA\}\}= engine\-exact robust\-safe set; boundary\-balanced evaluation,ε=0\.10\\varepsilon=0\.10,d=1d=1, 3 seeds,neval=800n\_\{\\mathrm\{eval\}\}=800/domain\. Point systems pay a boundary price; the gate\-certified Lipschitz backend holds policy false\-allow0\(Wilson 95% upper≤0\.022\\leq 0\.022\) while recovering≈0\.65\\approx 0\.65ofROPAR\_\{\\mathrm\{OPA\}\}\(the quantified learning tax vs the policy\-certified exact backend\)\. RS atnmc=800n\_\{\\mathrm\{mc\}\}=800is vacuous \(documented budget choice; Lipschitz is the primary\)\.Question\.Is the joint gap an artifact of one scale?Setting\.Three controlled sweeps×8000\\times\\,8000synthetic records,d=1d=1, action\-partitioned tool vocabularies\.Result\.Joint\-gap prevalence stays at7\.87\.8–9\.7%9\.7\\%, the certificate is sound at every point, and the uncertified learned gate’s attack false\-allow spans0\.900\.90–0\.980\.98— the9090–98%98\\%anchor \(Table[S8](https://arxiv.org/html/2607.29190#A5.T8)\)\.

Table S8:Scaling study \(Experiment A; anchors the uncertified9090–98%98\\%attack success\)\. Three sweeps×8000\\times\\,8000records,d=1d=1, synthetic typed tools with action\-partitioned vocabularies\. Joint\-gap prevalence stays7\.87\.8–9\.7%9\.7\\%, the certificate is sound at every point, and the uncertified learned gate’sattack\_false\_allowspans0\.900\.90–0\.980\.98while naive composition is1\.01\.0\.Question\.Where do the PSD2/AML anchors and the additional realistic\-schema and DevOps evaluations come from?Setting\.PSD2/AML source\-locked regulatory thresholds \(natural sampling\), realistic\-schema threshold\-gap policies \(50,00050\{,\}000records/domain\), and benchmark\-grounded DevOps fixtures\.Result\.Each setting’s provenance, sampling scheme, and oracle are pinned per row \(Table[S9](https://arxiv.org/html/2607.29190#A5.T9)\)\.

Table S9:Per\-setting anchors for PSD2/AML and the additional realistic\-schema and DevOps evaluations \(Experiments REG, B, G\)\. PSD2/AML: source\-locked regulatory thresholds \(PSD2 Art\. 11/16/18 exemption values, US CTR\), authored executably, natural sampling\. Realistic schemas:50,00050\{,\}000records/domain, synthetic threshold\-gap policies\. DevOps:9,6009\{,\}600benchmark\-grounded fixture records under thehybrid\_policyoracle \(boundary\-constructed, hence the higher witness share\); itsRallow≈0\.11R\_\{\\mathrm\{allow\}\}\\approx 0\.11is a conservative lower bound \(≈27%\\approx 27\\%analytically certifiable\)\.Question\.Does an adaptive attacker who knows the gate break it?Setting\.Adaptive in\-budget attack \(TM2\) against a locally\-correct learned gate and against the certified gate\.Result\.The learned gate admits true\-unsafe points; the certified gate removes them all \(0\.0000\.000\) while staying non\-vacuous onRR\(Table[S10](https://arxiv.org/html/2607.29190#A5.T10)\)\.

Table S10:Adaptive attack on the gate \(Section 6\.4\)\. A locally\-correct learned gate admits true\-unsafe points; the certified gate removes them \(0\.0000\.000\) while staying non\-vacuous onRR\.Question\.Does soundness survive held\-out shift?Setting\.Held\-out policies, schemas, and thresholds, with clean accuracy and certified false allow reported for each condition\.Result\.Certified and certified\-adversarial false allow are0in every condition; under threshold shift the learned gate degrades sharply, and both effects are reported rather than averaged away \(Table[S11](https://arxiv.org/html/2607.29190#A5.T11)\)\.

Table S11:Held\-out generalization \(Section 6\.4\)\. Soundness holds across all conditions \(cert\_false\_allow=\\texttt\{cert\\\_false\\\_allow\}=cert\. adv\. FA=0=0\); under threshold shift the learned gate degrades sharply and utility moves, and both are reported\. The headline numbers are reported inline \(Section 6\.4\); this table adds clean accuracy andcert\_false\_allow\.Question\.What does each of the two channels contribute on real features?Setting\.IEEE\-CIS features with display\-channel attacks \(fixed set of88, adaptive set of1313;n=120n=120/cell\) and theBd,εB\_\{d,\\varepsilon\}certificate over the typed return \(category\-balancedn=600n=600\)\.Result\.Point gates are locally correct yet keepCallow=1\.0C\_\{\\mathrm\{allow\}\}=1\.0; only the joint certificate closes the joint gap \(Table[S12](https://arxiv.org/html/2607.29190#A5.T12)\)\.

Table S12:Real\-data two\-channel run on IEEE\-CIS features \(Section 6\.4\): display\-channel attacks \(fixed set of 8 and adaptive set of 13\) against the untrusted text, and theBd,εB\_\{d,\\varepsilon\}certificate over the typed return; constructed provenance\-threshold policy,n=120n=120/cell \(display\) and category\-balancedn=600n=600\(certificate\)\. Point gates are locally correct yet keepCallow=1\.0C\_\{\\mathrm\{allow\}\}=1\.0; only the certified gate is sound, atRallow=0\.20R\_\{\\mathrm\{allow\}\}=0\.20\.Question\.What remains when there is no executable policy at all?Setting\.Policy = the real IEEE\-CISisFraudlabel \(gate AUC≈0\.72\\approx 0\.72\); exact and marginal certificates are undefined in this regime\.Result\.CAGE\-RS reduces empirical fraud exposure; the formal certificate remains a certificate of the smoothed gate, with the gate–policy fidelity gap made explicit \(Table[S13](https://arxiv.org/html/2607.29190#A5.T13)\)\.

Table S13:Implicit\-policy regime as a gate\-fidelity stress test \(Section 6\.4\): policy = the real IEEE\-CISisFraudlabel \(gate AUC≈0\.72\\approx 0\.72; no executable predicate, so exact and marginal certificates are undefined\)\. CAGE\-RS reduces empirical fraud exposure in this low\-fidelity regime, and the formal certificate remains a certificate of the smoothed gate: the gate–policy fidelity assumption stays\. The deterministic backend keeps a stable certified fraction at low sample size where smoothing collapses; ground truth is the held\-out fraud label \(empirical, never a predicate\-soundness theorem\)\.
### E\.2End\-to\-end systems and comparators

Real LLM proposers, deployed\-defense comparators, and committed side effects on real engines\.

#### Engine\-verified joint\-gap witnesses \(Section 6\.2\)\.

The provenance\-conditioned idiomrisk\_score<θ​\(provenance\)\\texttt\{risk\\\_score\}<\\theta\(\\text\{provenance\}\)is authored executably with the real generation constants \(θ=0\.488808\\theta=0\.488808,δ=0\.08\\delta=0\.08\), once as Rego and once as a JDM decision table, and every point of the probe set \(clean, thed=1d\{=\}1loose↔\\leftrightarrowstrict provenance swap, the\+ε\+\\varepsilonnumeric move, and the joint swap\+ε\+\\varepsilon\) is labelled by the engine itself over real boundary\-balanced IEEE\-CIS transactions\. Both engines, OPA 1\.17\.1 and GoRules ZEN 0\.53 \(a Rust decision engine used in fintech\), label800800category\-CCwitnesses over40004000transactions each and reproduce the analytic taxonomy exactly \(engine–analytic agreement1\.0001\.000,CC\-set Jaccard1\.0001\.000\)\. The20%20\\%rate is the engineered balanced\-set rate; natural prevalence is≈6\.4%\\approx 6\.4\\%\(Table[S1](https://arxiv.org/html/2607.29190#A5.T1)\)\. Neither engine is a purpose\-built fraud/AML engine: the claim is engine independence of the joint gap, and deployed\-rule discovery remains a separate question\. A purpose\-built AML engine confirms the same labels \(Table[S21](https://arxiv.org/html/2607.29190#A5.T21)\), and a second independent adapter reproduces both the taxonomy and the marginal\-vs\-joint verdicts through real Kyverno admission \(Table[S23](https://arxiv.org/html/2607.29190#A5.T23)\)\.

Question\.Is the threat model\-dependent while the defense is model\-independent?Setting\.Four real proposers \(three Qwen2\.5 variants and the 36B\-MoEqwen3\.6\) proposing actions on IEEE\-CIS, mock control included\.Result\.Undefended leak varies substantially across models and domains; the measured certified false\-allow rate is0\.0000\.000for every model and domain, and gate\-level outcomes are identical across proposers, which pre\-gate approve100%100\\%of category\-CCtransactions \(Tables[S14](https://arxiv.org/html/2607.29190#A5.T14)–[S15](https://arxiv.org/html/2607.29190#A5.T15)\)\.

Table S14:Model\-dependent threat vs\. model\-independent defense \(Section 6\.4\)\. Undefended leak \(oraclecert\_false\_allowunder the joint\-gap attack\) varies substantially across models and domains; the certified gate is0\.0000\.000for every model and domain\. Parse rate1\.0001\.000for all models; certifiedRexecR\_\{\\mathrm\{exec\}\}\(finance\)0\.3420\.342\(32B\) and0\.3500\.350\(qwen3\.6\)\.Table S15:Real\-LLM action proposal on IEEE\-CIS \(Section 6\.4\), unsafe execution rate\. Gate\-level outcomes are identical across mock, 7B, and 32B; the model\-dependent threat is in Table[S14](https://arxiv.org/html/2607.29190#A5.T14)\. Pre\-gate, both 7B and 32B approve100%100\\%of category\-CCtransactions \(paired display\-only flip rate0\.730\.73–0\.930\.93\) and comply with100%100\\%of display\-channel injections\.Question\.Can untrusted display text steer unsafe execution through a typed gate?Setting\.Display\-channel injections \(TM1\) against every system, including a robust prompt and a third model \(qwen3\.6\)\.Result\.Display text moves the LLM proposal for every system, but typed gates make unsafe execution invariant to it \(spread0\.000\.00\); a robust prompt does not fix the undefended systems \(Table[S16](https://arxiv.org/html/2607.29190#A5.T16)\)\.

Table S16:Non\-instructability \(TM1; Section 6\.4\)\. Display textmmmoves the LLM proposal for every system, but typed gates make unsafe execution invariant tomm\(spread0\.000\.00\)\. A robust prompt does not fix it\. Reproduced with a third model \(EXP\-C3,qwen3\.636B MoE\): undefendedunsafe\_exec0\.850\.85–1\.001\.00,llm\_flip0\.800\.80–0\.830\.83, typed gates invariant \(gate\_flip=0\\texttt\{gate\\\_flip\}=0\); best\-of\-KKpushes the strongest prompt baseline to0\.1000\.100while the typed gate holds0\.Question\.Can an LLM judge substitute for the certificate?Setting\.Judges evaluate the serialized observed pair\(z,a\)\(z,a\)on the witness set; a budget\-aware judge additionally receives the exactBd,εB\_\{d,\\varepsilon\}and is asked for the worst case \(33seeds, benign paraphrases\)\.Result\.The budget\-aware judge’s verdict spans the full\[0,1\]\[0,1\]across three benign paraphrases of the same instruction: not a sound gate \(Table[S17](https://arxiv.org/html/2607.29190#A5.T17)\)\.

Table S17:LLM\-judge baselines on the witness setWW\(Section 6\.2\)\. Judges evaluate the serialized observed pair\(z,a\)\(z,a\); the certified gate evaluatesBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\)\. The budget\-aware judge receives the exactBd,εB\_\{d,\\varepsilon\}in its prompt and is asked for the worst case; its verdict spans the full\[0,1\]\[0,1\]across three benign paraphrases of the same instruction \(33seeds each, decode temperature0\.70\.7\)\. Judge modelqwen2\.5:32b\(Qwen Team[2024](https://arxiv.org/html/2607.29190#bib.bib41)\); guard modelllama\-guard3:1b\(Inanet al\.[2023](https://arxiv.org/html/2607.29190#bib.bib34)\)\.cert\_false\_allowis the empirical fraction of allows that are joint\-unsafe\. Stronger\-judge leg \(EXP\-C3\):qwen3\.6\(36B MoE, chain\-of\-thought off\) at decode temperature0\.70\.7and0; at temperature0the three decode seeds are identical per phrasing \(one phrasing0\.6170\.617, the others0\.0000\.000\), so the residual spread is phrasing sensitivity, not sampling noise\. A tool\-augmented judge that reproduced the enumeration would concede the locus argument\.Question\.Do deployed defense hooks admit the joint\-gap witness?Setting\.Runtime enforcement of the observed action \(AgentSpec, VeriGuard\), the capability defense CaMeL, and pre\-execution screening, all on the same witness set \(Experiment P5\)\.Result\.A witness is safe at the observed point, so every point\-evaluating defense admits it; only the joint certificate blocks it, and CaMeL and the certificate are orthogonal \(Table[S18](https://arxiv.org/html/2607.29190#A5.T18)\)\.

Table S18:Deployed\-defense comparators \(Experiment P5; Sections 2 and 6\.3\)\.*Summary:*a joint\-gap witness is safe at the observed point, so every point\-evaluating defense admits it; runtime enforcement of the observed action \(AgentSpec\(Wanget al\.[2026a](https://arxiv.org/html/2607.29190#bib.bib26)\), VeriGuard\(Miculicichet al\.[2025](https://arxiv.org/html/2607.29190#bib.bib25)\)\) and the capability defense CaMeL\(Debenedettiet al\.[2025](https://arxiv.org/html/2607.29190#bib.bib13)\)both allow it, and only the neighborhood certificate blocks it\.∗CaMeL is orthogonal rather than dominated: on the real finance schema it blocks source\-tainted values that CAGE allows and admits the in\-scope\-provenance witness that CAGE blocks, so the two are composable and neither subsumes the other \(*orthogonality*rows\)\.*Classifier:*a maximally generous pre\-execution transcript classifier \(full transcript, point accuracy1\.001\.00\) used as an authorize\-then\-realize gate still commits unsafe effects at the no\-gate rate on joint\-gap witnesses, while the joint certificate commits none; cleanCC\-vs\-RRseparation AUC is0\.540\.54–0\.650\.65: the distinction lives inBd,εB\_\{d,\\varepsilon\}, not at the point\.Question\.Does non\-composition realize as committed side effects end\-to\-end?Setting\.Full agent chain with committed effects \(money approved / alert suppressed\),300300episodes per \(domain, attack\), finance and SRE\.Result\.Under the joint\-gap attack the composed marginal certificates commit unsafe effects at the full no\-gate rate; the joint certificate commits none \(Table[S19](https://arxiv.org/html/2607.29190#A5.T19)\)\.

Table S19:End\-to\-end unsafe commits \(Section 6\.3\): full chain with committed side effects \(money approved / alert suppressed\),300300episodes per \(domain, attack\), finance/SRE\. Under the joint\-gap attack the analytic marginal certificate commits unsafe effects at the no\-gate rate: composing two sound marginal certificates produces concrete unsafe commits, the non\-composition thesis realized end\-to\-end\. The joint certificate stays non\-vacuous on clean traffic \(privileged\-execution rates0\.230\.23finance /0\.1170\.117SRE, all safe\)\.Question\.Does the exploit and its defense hold on a live cluster?Setting\.Akindcluster \(Kubernetes v1\.31\) with real Kyverno v1\.13 admission; the tier is resolved from a registry ConfigMap \(the TOCTOU surface\) serving a stalelaxtier while the true tier isstrict\.Result\.The over\-provisioned workload is admissible under the served binding and blocked by the certified gate, with the matching safe control passing \(Table[S20](https://arxiv.org/html/2607.29190#A5.T20)\)\.

Table S20:Real\-harness integration \(Experiments P3, P3\-MCP, P3\-mediation, P3\-A8; Section 6\.3\)\. A livekindcluster \(Kubernetes v1\.31\) with real Kyverno v1\.13 admission resolves the tier from a separate registry ConfigMap \(the TOCTOU surface\); the registry serves a stalelaxtier while the true tier isstrict, so a six\-replica workload is admissible under the served binding and unsafe under the true one\. The certified gate \(rung 1\) enumerates the tier neighborhood, tests theε\\varepsilon\-shifted cap on every branch, and blocks before the call; with a fresh registry Kyverno itself denies, matching the gate; a genuinely safe workload deploys \(non\-vacuous\)\. Gate overhead≈0\.3​μ\\approx 0\.3\\,\\mus per decision \(≈10​μ\\approx 10\\,\\mus on the MCP path, vs≈2\.5\\approx 2\.5s LLM decode\)\. Four real proposers \(three Qwen2\.5 variants andqwen3\.6\) all submit the unsafe apply through a real MCP write path\. Integration illustrations only: the certified object remainsAllow⁡\(z,a\)\\operatorname\{Allow\}\(z,a\)\.Question\.Does a deployed\-grade AML engine reproduce the taxonomy and the exploit?Setting\.The idiomrisk\_score<θ​\(provenance\)\\texttt\{risk\\\_score\}<\\theta\(\\text\{provenance\}\)authored as a Marble v1\.4\.0 scenario with the real IEEE\-CIS constants; probes and end\-to\-end commits run through the engine’s own decision API\.Result\.The engine labels the four probes exactly as the taxonomy predicts, and every ungated approval is persisted by the engine while the certified run commits none \(Tables[S21](https://arxiv.org/html/2607.29190#A5.T21)–[S22](https://arxiv.org/html/2607.29190#A5.T22)\)\.

Table S21:Purpose\-built AML\-engine verification of the joint\-gap taxonomy \(B2\-Marble; Section 6\.2\)\. The idiomrisk\_score<θ​\(provenance\)\\texttt\{risk\\\_score\}<\\theta\(\\text\{provenance\}\)is authored as a Marble v1\.4\.0 scenario with the real IEEE\-CIS constants and published; real transactions are run through the engine’s own decision API, which labels the four probes \(clean,d=1d\{=\}1provenance swap,\+ε\+\\varepsilon, joint swap\+ε\+\\varepsilon\) per record\. Claim discipline: a real deployed\-grade AML engine executing an*authored*rule on real data: engine\-verified existence, one level above the general\-purpose engines \(OPA, GoRules ZEN\), not a claim the rule was mined from a bank’s deployed policies\.Table S22:Committed side effects on a deployed\-grade AML engine \(Experiment B2\-Marble e2e; Section 6\.3\)\. The pipeline serves the stale loose provenance; the gate certifiesBd,ε​\(z\)B\_\{d,\\varepsilon\}\(z\)around the served return; on allow the adversary realizes the in\-budget worst case\. Every ungated approval is committed and persisted by Marble’s own decision API \(verified viaGET /v1/decisions\); the certified gate submits none of them and stays non\-vacuous; Marble itself reviews every realized worst case, agreeing with the gate\.100100joint\-gap witnesses \+100100robust\-safe controls, real IEEE\-CIS transactions,ε=0\.10\\varepsilon=0\.10\.Question\.Does a second, independent real adapter reproduce the taxonomy?Setting\.Kubernetes Deployment manifests mapped toz=\(tier,cost\)z=\(\\texttt\{tier\},\\texttt\{cost\}\), with real Kyverno admission enforcingcost≤θ​\(tier\)\\texttt\{cost\}\\leq\\theta\(\\texttt\{tier\}\)from a ConfigMap\.Result\.A different domain, return format, and threshold family reproduce the same A/B/C/R/U structure \(Table[S23](https://arxiv.org/html/2607.29190#A5.T23)\)\.

Table S23:Second independent real adapter \(Experiment A7; Section 6\.2\)\. A Kubernetes Deployment manifest maps toz=\(tier,cost\)z=\(\\texttt\{tier\},\\texttt\{cost\}\)and real Kyverno admission enforcescost≤θ​\(tier\)\\texttt\{cost\}\\leq\\theta\(\\texttt\{tier\}\)with the threshold resolved from a ConfigMap \(θstrict=0\.50\\theta\_\{\\mathrm\{strict\}\}=0\.50,θloose=0\.80\\theta\_\{\\mathrm\{loose\}\}=0\.80,ε=0\.10\\varepsilon=0\.10\): a different domain, return format, and engine from the IEEE\-CIS adapters\. The engine admits every single\-channel move and denies the joint one, so naive marginal composition false\-allows on the engine itself\.

### E\.3External\-validity evidence

The frozen\-scan evidence hierarchy and the third\-party deployed\-rule anchor\.

Question\.What exactly is claimed at each level of external validity?Setting\.An evidence hierarchy kept separate by provenance: third\-party existence, regulatory\-grounded continuous mechanism, and engine\-validated defense\.Result\.Existence of the idiom is anchored in third\-party code and quantized cloud policy; the continuous mechanism uses source\-locked regulatory thresholds; deployment prevalence is explicitly not claimed \(Table[S24](https://arxiv.org/html/2607.29190#A5.T24)\)\.

Table S24:Evidence hierarchy for external validity \(Section 6\.4\), kept separate by provenance\. Existence of the category\-conditioned\-threshold idiom is anchored in third\-party code; the continuous mechanism and the certified defense use source\-locked regulatory thresholds and an executable policy\-as\-code engine, respectively\. Per\-corpus counts behind Section 6\.4:≈1424\\approx 1424k8s/cloud policies \(39 numeric thresholds, 0 provenance\-keyed\); 43 MCP reference tools \(29 untyped, substrate 0\); 4138 OpenAPI specs / 701 providers \(structural co\-occurrence9\.8%9\.8\\%, finance habitat22\.4%22\.4\\%, confirmed pipeline\-set 0\); MCP registries: 1085 servers / 5002 tools, substrate5\.0%5\.0\\%of typed returns \(Wilson 95%\[3\.5,7\.0\]%\[3\.5,7\.0\]\\%, threat\-intel/content/bibliographic\); DMN\-TCK4\.9%4\.9\\%/ Kogito11\.5%11\.5\\%; OpenFisca6\.8%6\.8\\%\(subject\-keyed\)\.Question\.Does the candidate substrate survive conservative adjudication?Setting\.Two\-pass Stage\-2 adjudication \(lexical \+ frozen semantic table, disagreement⇒\\RightarrowOUT\) of the3131Stage\-1 candidates across88servers; zero execution\.Result\.The5\.0%5\.0\\%candidate habitat collapses to a fourth informative null; the structural residual is named rather than hidden \(Table[S25](https://arxiv.org/html/2607.29190#A5.T25)\)\.

Table S25:Registry\-scale substrate adjudication \(EXP\-A2; Section 6\.4\)\. Conservative two\-pass Stage\-2 adjudication of the 31 Stage\-1 candidates \(8 servers, frozen detector\): the5\.0%5\.0\\%candidate habitat collapses to a fourth informative null; the structural residual is named, not hidden\. Zero\-execution \(published schemas\)\.Question\.How prevalent is the structural idiom in committed third\-party rule code?Setting\.The frozen Phase\-1 detector applied through additional format parsers to legislation\-as\-code, decision\-table, and rule\-engine corpora\.Result\.Structural presence reaches4\.94\.9–11\.5%11\.5\\%, but in every hit the selector is a subject/status attribute:provenance\_upstream\_rate=0\\texttt\{provenance\\\_upstream\\\_rate\}=0\(Table[S26](https://arxiv.org/html/2607.29190#A5.T26)\)\.

Table S26:Structural prevalence and per\-engine idiomaticity ofop​\(fnum,θ​\(s\)\)\\mathrm\{op\}\(f\_\{\\mathrm\{num\}\},\\theta\(s\)\)in third\-party committed rule code \(Experiments P1\-B, A\-DMN, B1; frozen Phase\-1 detector, detector integrity hashes recorded\)\.*Top:*structural rates in committed corpora; in every hit the selectorssis a subject/status attribute, soprovenance\_upstream\_rate=0\\texttt\{provenance\\\_upstream\\\_rate\}=0\(structural presence, distinct from security\-relevant prevalence\)\.*Bottom:*per\-engine expressibility inventory \(no rate emitted\): the idiom is a first\-class construct in decision\-table engines and purpose\-built AML engines, expressible\-but\-generic elsewhere\.Question\.Does a verbatim third\-party policy instantiate the mechanism?Setting\.OpenFisca\-France Bail Réel Solidaire income ceilingsθ​\(zone,household\)\\theta\(\\mathrm\{zone\},\\mathrm\{household\}\)at a frozen commit, used unmodified;𝒩d\\mathcal\{N\}\_\{d\}= the policy’s own five zones,n=20n=20k\.Result\.The point gate admits all1,7731\{,\}773joint\-gap witnesses and the exact certificate admits none; the zone key is subject\-set, so the claim is scoped accordingly \(Table[S27](https://arxiv.org/html/2607.29190#A5.T27)\)\.

Table S27:Independent third\-party policy case study \(EXP\-CX5; Section 6\.4\)\. OpenFisca\-France, Bail Réel Solidaire income ceilingsθ​\(zone,household\)\\theta\(\\mathrm\{zone\},\\mathrm\{household\}\)\(frozen commita9d8dcbe, transcribing Arrêté du 11/12/2023 / Art\. R255\-1 CCH\); the rule is used verbatim,𝒩d\\mathcal\{N\}\_\{d\}= its own five zones,n=20n=20k\. Scope: zone is a subject/region attribute, not a pipeline\-provenance key: this is a deployed\-threshold*existence*anchor, complementary to the pipeline\-provenance nulls \(S24, S25\)\.
### E\.4Threat\-model calibration and residual risk

Budget calibration, discrete\-channel and freshness escape, and negative controls\.

Question\.Do correlated faults exceed the declared discrete budget?Setting\.Compound fault injection \(pairs and triples\) with realized flip mass measured per clean category \(EXP\-A1\)\.Result\.All fault pairs land atd≤2d\\leq 2\(fracd≤2=1\.000\\mathrm\{frac\}\_\{d\\leq 2\}=1\.000\) and thed=2d=2Lipschitz gate stays sound withRallow=0\.40R\_\{\\mathrm\{allow\}\}=0\.40–0\.750\.75\(Table[S28](https://arxiv.org/html/2607.29190#A5.T28)\)\.

Table S28:Compound / correlated fault injection \(EXP\-A1; Table[8](https://arxiv.org/html/2607.29190#S6.T8)and Section 6\.5\)\. All fault*pairs*land atd≤2d\\leq 2\(fracd≤2=1\.000\\mathrm\{frac\}\_\{d\\leq 2\}=1\.000\); thed=2d=2Lipschitz gate stays sound \(cert\_false\_allow=0\\texttt\{cert\\\_false\\\_allow\}=0,fscale=3f\_\{\\mathrm\{scale\}\}=3,Rallow=0\.40R\_\{\\mathrm\{allow\}\}=0\.40–0\.750\.75\)\. Realized C→\\toU flip mass is measured per clean category \(e\.g\. financestale\_cache\+wrong\_provenance:13\.6%13\.6\\%of clean\-CCrecords, adversarial regime\)\.40004000samples/combo×\\times3 seeds, real IEEE\-CIS \+ finance/SRE\.Question\.What does raising the discrete budget cost?Setting\.d∈\{1,2,3\}d\\in\\\{1,2,3\\\}with exact𝒩d\\mathcal\{N\}\_\{d\}enumeration, deterministic Lipschitz backend, both tracks,33seeds\.Result\.Sound at everyddon both tracks with graceful utility decay; the numeric scaling is held\-out validated \(Table[S29](https://arxiv.org/html/2607.29190#A5.T29)\)\.

Table S29:Discrete\-budget sweepd∈\{1,2,3\}d\\in\\\{1,2,3\\\}\(Section 6\.5\), exact𝒩d\\mathcal\{N\}\_\{d\}enumeration, deterministic Lipschitz backend, both tracks numeric\-scaled \(OPAfscale=3\\texttt\{fscale\}=3, synthetic44: the largest values keepingcert\_false\_allow=0\\texttt\{cert\\\_false\\\_allow\}=0at everydd; held\-out selection hygiene in Table[S45](https://arxiv.org/html/2607.29190#A5.T45)\);33seeds\. Sound at everyddon both tracks with graceful utility decay; the RS ablation instead collapses through its per\-branch correctionα/\|𝒩d\|\\alpha/\|\\mathcal\{N\}\_\{d\}\|\(OPA0\.05→0→00\.05\\to 0\\to 0; synthetic0\.39→0\.090\.39\\to 0\.09\)\.\|𝒩d\|\|\\mathcal\{N\}\_\{d\}\|grows8→24→368\\to 24\\to 36\(OPA\) and18→109→25618\\to 109\\to 256\(synthetic\|X1\|=8\|X\_\{1\}\|\{=\}8\), cost ratio1/4\.7/9\.91/4\.7/9\.9; the operational enumeration cliff isd≈2d\\approx 2, where\|𝒩d\|\|\\mathcal\{N\}\_\{d\}\|reaches2424–109109across tracks\. OPAfscale≥4\\texttt\{fscale\}\\geq 4liftsRallowR\_\{\\mathrm\{allow\}\}but breaks soundness atd≥2d\\geq 2\.Question\.Which fault mechanisms escape the discrete neighborhood?Setting\.Leave\-one\-fault\-out: rebuild𝒩d\\mathcal\{N\}\_\{d\}without each mechanism and measure the escape probability on real substrates \(33seeds,ε=0\.10\\varepsilon=0\.10\)\.Result\.Provenance, policy\-pack, and TOCTOU faults never escape; the two escaping faults have no discrete footprint and are exactly what the validation stack targets \(Table[S30](https://arxiv.org/html/2607.29190#A5.T30)\)\.

Table S30:Discrete\-channel escape, leave\-one\-fault\-out \(Section 6\.5\): rebuild𝒩d\\mathcal\{N\}\_\{d\}without each mechanism and measurePr⁡\[z′∉𝒩d−M×Bε\]\\Pr\[z^\{\\prime\}\\notin\\mathcal\{N\}\_\{d\}^\{\-M\}\\times B\_\{\\varepsilon\}\]\(real IEEE\-CIS / finance / SRE substrates,33seeds,ε=0\.10\\varepsilon=0\.10\)\. Provenance, policy\-pack, and TOCTOU faults never escape; the two escaping faults have no discrete footprint \(they driftxxpastε\\varepsilon, the out\-of\-budget tail scoped to validation\)\. Over\-declaringKKinert branches costs utility:Rallow=0\.172/0\.109/0\.051/0\.012/0\.002R\_\{\\mathrm\{allow\}\}=0\.172/0\.109/0\.051/0\.012/0\.002atK=0/1/2/4/8K=0/1/2/4/8\(\|𝒩d\|​3→11\|\\mathcal\{N\}\_\{d\}\|\\ 3\\to 11\)\.Question\.What continuous residual does each covered fault carry?Setting\.40004000samples per fault, measured after the integrity\+freshness validation stack \(Experiment FAULT\)\.Result\.Discrete binding faults carry no continuous drift; the pooledεemp​@​p95≈0\.079\\varepsilon\_\{\\mathrm\{emp\}\}@\\mathrm\{p95\}\\approx 0\.079–0\.0950\.095anchors Table[8](https://arxiv.org/html/2607.29190#S6.T8)\(Table[S31](https://arxiv.org/html/2607.29190#A5.T31)\)\.

Table S31:Per\-fault continuous residuals \(Experiment FAULT,40004000samples/fault; anchors Table[8](https://arxiv.org/html/2607.29190#S6.T8)’s pooledεemp​@​p95≈0\.079\\varepsilon\_\{\\mathrm\{emp\}\}@\\mathrm\{p95\}\\approx 0\.079–0\.0950\.095, measured after the integrity\+freshness validation stack\)\. Discrete binding faults carry no continuous drift; the two out\-of\-budget mechanisms are exactly those a schema/identity validation layer targets\.Question\.What does the certificate explicitly not cover?Setting\.Fabricated returns with gap≤ε\\leq\\varepsilonversus gap≫ε\\gg\\varepsilon\(negative control\)\.Result\.The in\-budget lie is refused; far outside the budget the certificate makes no claim and a sound gate allows the fabricated return — the boundary of the guarantee, stated \(Table[S32](https://arxiv.org/html/2607.29190#A5.T32)\)\.

Table S32:Negative control \(Appendix E\.4\)\. Forgap≤ε\\texttt\{gap\}\\leq\\varepsilonthe lie is inside the budget and the gate refuses; forgap≫ε\\texttt\{gap\}\\gg\\varepsilonthe certificate makes no claim and a sound gate allows the fabricated return\.Question\.Where does the declared budget actually break?Setting\.The model\-free robust\-oracle certificate forB1,0\.10B\_\{1,0\.10\}held fixed while the adversary moves strictly outside it \(Experiment P2\)\.Result\.False allow over certified allows is0at every in\-budget point and first leaves zero atε∗=0\.11\\varepsilon^\{\*\}=0\.11,d∗=2d^\{\*\}=2\(Table[S33](https://arxiv.org/html/2607.29190#A5.T33)\)\.

Table S33:Breaking radius of the declared budget \(Experiment P2; Section 6\.5\)\. The model\-free robust\-oracle certificate forB1,0\.10B\_\{1,0\.10\}is held fixed while the adversary moves strictly outside it; the false\-allow rate over certified allows is0at every in\-budget point and first leaves zero atε∗=0\.11\\varepsilon^\{\*\}=0\.11andd∗=2d^\{\*\}=2\(d=3d=3adds nothing: the schema exhausts its discrete atoms atd=2d=2\): degradation is graceful and visible, never a silent in\-budget false allow\. Mechanism placement matches Table[8](https://arxiv.org/html/2607.29190#S6.T8): the in\-budget provenance fault leaks0\.0000\.000; stale cache0\.014/0\.0180\.014/0\.018; schema skew0\.089/0\.0280\.089/0\.028; cache key collision \(εp​95≈1\.2\\varepsilon\_\{p95\}\\approx 1\.2,12×12\\timesthe budget\)0\.325/0\.2440\.325/0\.244\. Scope probe \(Experiment SEL\): a metadata\-poisoning mis\-selection within the gated action group is ad=1d=1provenance swap the certificate already covers \(unsafe execution1\.00→0\.001\.00\\to 0\.00\); a cross\-action mis\-selection lies outside the per\-action ball and retains a0\.310\.31residual: tool selection stays an upstream defense surface\.Question\.What happens when the trusted constructor itself is corrupted?Setting\.A field flip with probabilityppat thezz\-constructor, below the typed interface \(55seeds\)\.Result\.False allow grows monotonically withpp, delimiting where the guarantee stops; this anchors the1\.7%1\.7\\%trust\-boundary number \(Table[S34](https://arxiv.org/html/2607.29190#A5.T34)\)\.

Table S34:Constructor\-corruption sweep \(EXP2, part B; anchors the1\.7%1\.7\\%trust\-boundary number\)\. A field flip with probabilityppat thezz\-constructor, below the typed interface; the verified\-point gate trusts the delivered provenance\. False allow grows monotonically withpp, delimiting where the guarantee stops;55seeds\.Question\.What freshness SLA keeps the declared budget valid?Setting\.Same\-card wall\-clock staleness on real IEEE\-CIS: a fine sub\-minute gridΔ​t∈\{1,…,120\}\\Delta t\\in\\\{1,\\dots,120\\\}s \(55seeds, coverage\-aware\) and the coarse grid plotted in Figure 4\.Result\.Certified false allow is0at everyΔ​t\\Delta t, but no well\-covered sub\-minute SLA meets a<1%<1\\%system escape: scores must be recomputed in\-loop \(Tables[S35](https://arxiv.org/html/2607.29190#A5.T35)–[S36](https://arxiv.org/html/2607.29190#A5.T36)\)\.

Table S35:Sub\-minute freshness\-SLA sweep \(EXP\-A3; Section 6\.5\)\. Fine gridΔ​t∈\{1,…,120\}\\Delta t\\in\\\{1,\\dots,120\\\}s on real IEEE\-CIS same\-card wall\-clock staleness, 5 seeds, coverage\-aware\.cert\_false\_allow=0\\texttt\{cert\\\_false\\\_allow\}=0at everyΔ​t\\Delta t; no well\-covered sub\-minute SLA meets a<1%<1\\%system escape, so scores must be recomputed in\-loop\.Table S36:Coarse freshness\-SLA grid \(Experiment EXP2\-A; the points Figure 4 plots\)\. Same\-card wall\-clock staleness on real IEEE\-CIS;cert\_false\_allow=0\\texttt\{cert\\\_false\\\_allow\}=0at everyΔ​t\\Delta t; the fine sub\-minute grid is Table S35\.Question\.What does the normalizedε=0\.10\\varepsilon=0\.10mean in raw units?Setting\.The raw\-unit move corresponding to a normalizedε\\varepsilonstep, per field and anchor\.Result\.Per\-field raw\-unit equivalents \(marginal view; the jointℓ2\\ell\_\{2\}ball couples fields, so single\-field values are upper bounds\) \(Table[S37](https://arxiv.org/html/2607.29190#A5.T37)\)\.

Table S37:Raw\-unitε\\varepsilonaudit \(EXP\-B2; Section 6\.5 and Appendix D\)\. The raw\-unit move corresponding to a normalizedε=0\.10\\varepsilon=0\.10step, per field and anchor \(marginal per\-field view; the jointℓ2\\ell\_\{2\}ball couples fields, so single\-field values are upper bounds\)\.Question\.Do calibrated per\-field budgets beat one isotropicε\\varepsilon?Setting\.Multivariate\-affine policy \(k=6k=6\), exact certificates with each geometry’s dual norm, every geometry calibrated on a frozen split to the same held\-out fault coverage \(q=0\.95q=0\.95\),55seeds\.Result\.The comparison is coverage\-matched by construction; the residual≈0\.038\\approx 0\.038policy false allow is the calibration escape — the5%5\\%fault tail beyond the frozen quantile \(Table[S38](https://arxiv.org/html/2607.29190#A5.T38)\)\.

Table S38:Calibrated per\-field budget \(EXP\-CX4; Section 6\.5\)\. Multivariate\-affine policy \(k=6k=6\), exact certificate with the dual norm of each geometry; every geometry calibrated on a frozen split to the same held\-out joint fault coverage \(q=0\.95q=0\.95\), evaluated disjointly, 5 seeds\. The residual≈0\.038\\approx 0\.038policy false\-allow is the calibration escape \(the5%5\\%fault tail beyond the frozen budget\), identical across geometries: not certificate unsoundness\. Real IEEE\-CIS anchor: per\-field p95 residual heterogeneity2\.9×2\.9\\times\(0\.0550\.055vs0\.0190\.019\)\.Question\.Does budget calibration survive a real adapter into a real engine?Setting\.The Table[8](https://arxiv.org/html/2607.29190#S6.T8)fault mechanisms run through a real adapter into Marble’s decision API;εcal=0\.052\\varepsilon\_\{\\mathrm\{cal\}\}=0\.052is the p95 residual on a calibration half \(Experiment CX6\)\.Result\.The calibrated budget holds held\-out, leaking only outside the ball \(Table[S39](https://arxiv.org/html/2607.29190#A5.T39)\)\.

Table S39:Real\-adapter budget calibration through the Marble engine \(Experiment CX6; Section 6\.5\)\. The Table[8](https://arxiv.org/html/2607.29190#S6.T8)fault mechanisms run through a real adapter into Marble’s decision API;εcal=0\.052\\varepsilon\_\{\\mathrm\{cal\}\}=0\.052is the p95 residual under integrity\+freshness faults on a calibration half, and escape \(a fault that flips the engine’s decision yet falls outsideB1,εcalB\_\{1,\\varepsilon\_\{\\mathrm\{cal\}\}\}\) is measured on a disjoint holdout \(n=800n=800real IEEE\-CIS transactions,16581658unique engine decisions\)\. The calibrated budget generalizes; the schema/identity tail is the measured out\-of\-budget escape, scoped to the validation layer\.Question\.Does typed\-state projection restore fidelity at high ambient dimension?Setting\.A scalar policy onkactive=5k\_\{\\mathrm\{active\}\}=5fields padded with nuisance dimensions tokraw∈\{20,50,100\}k\_\{\\mathrm\{raw\}\}\\in\\\{20,50,100\\\}; four gates differing only in the fields they may use, same smoothed certificate, scored against the true oracle\.Result\.The dense gate reproduces thek=100k=100fidelity edge; the projected gate removes it \(Table[S40](https://arxiv.org/html/2607.29190#A5.T40)\)\.

Table S40:Policy\-state projection \(Experiment D\.4; Section 6\.5\)\. A scalar policy depends onkactive=5k\_\{\\mathrm\{active\}\}=5fields, padded with nuisance dimensions tokraw∈\{20,50,100\}k\_\{\\mathrm\{raw\}\}\\in\\\{20,50,100\\\}; four gates differ only in the fields they may use, with the same smoothed certificate, scored against the true oracle\. The dense gate reproduces thek=100k=100fidelity edge of Table[S46](https://arxiv.org/html/2607.29190#A5.T46); projecting to the low\-dimensional policy state removes it\. The certifiable interface is a typed low\-dimensional policy state rather than the raw record: the recommendation is projection, not smoothing the raw space\.Question\.Can abstention itself be weaponized \(availability, not safety\)?Setting\.Boundary\-seeking input selection against the exact analytic certificate on real IEEE\-CIS \(33seeds\)\.Result\.The attack inflates abstention but never safety: certified false allow stays0under benign and every adversarial strength; rate\-limit mitigations are noted \(Table[S41](https://arxiv.org/html/2607.29190#A5.T41)\)\.

Table S41:Abstention\-DoS \(Section 7\): boundary\-seeking input selection against the exact analytic certificate on real IEEE\-CIS \(33seeds;θbase=0\.4888\\theta\_\{\\mathrm\{base\}\}=0\.4888,δ=0\.08\\delta=0\.08,ε=0\.10\\varepsilon=0\.10\)\. The attack inflates abstention \(availability\) but never safety:cert\_false\_allow=0\\texttt\{cert\\\_false\\\_allow\}=0under benign and every adversarial strength\. Mitigations: a per\-source rate limit caps abstention at0\.370\.37\(cost:0\.840\.84of adversarial volume dropped\); adaptive\-ε\\varepsilonreclaims availability \(0\.99→0\.750\.99\\to 0\.75abstention atε=0\.02\\varepsilon=0\.02\) at residual exposure0\.240\.24;cert\_false\_allow=0\\texttt\{cert\\\_false\\\_allow\}=0under both\. The boundary\-balanced pool makes the benign floor conservative\.
### E\.5Reproducibility and statistical audits

Cost, monitoring, selection hygiene, horizon corrections, and the zero\-cell audit\.

Question\.What does each backend cost per decision, and what does the cost buy?Setting\.Per\-decision latency on the reference machine of Appendix D, pointwise gates included\.Result\.Pointwise gates are fast but unsound under an in\-budget adversary; certified cost is backend\-indexed \(exact<1​μ<1\\,\\mus, Lipschitz≈7\.8\\approx 7\.8ms, smoothing≈10\\approx 10–4646ms\) \(Table[S42](https://arxiv.org/html/2607.29190#A5.T42)\)\.

Table S42:Validity regime: per\-decision cost and soundness \(Section 6\.5\)\. Pointwise gates are fast but unsound under an in\-budget adversary; cost among the certified backends is backend\-indexed \(exact<<1μ\\mus, Lipschitz≈7\.8\\approx 7\.8ms, smoothing≈10\\approx 10–4646ms\)\. The smoothing rows are on the MLP backend\.Question\.Can gate–policy fidelity drift be monitored in operation?Setting\.A two\-window delayed\-audit detector over the real IEEE\-CIS gate pool, swept over audit delay, window size, and alarm threshold \(33seeds\), with an anytime\-valid upper bound\.Result\.The monitor detects fidelity drift from audited allows alone, providing the operational complement to the one\-shot certificates \(Table[S43](https://arxiv.org/html/2607.29190#A5.T43)\)\.

Table S43:Operational fidelity monitor \(EXP\-A4; Section 7\)\. Two\-window delayed\-audit detector over the real IEEE\-CIS gate pool \(baseline auditedcert\_false\_allow≈0\.28\\texttt\{cert\\\_false\\\_allow\}\\approx 0\.28–0\.340\.34, the weak implicit signal\);Δaudit∈\{1​h,1​d,7​d\}\\Delta\_\{\\mathrm\{audit\}\}\\in\\\{1\\mathrm\{h\},1\\mathrm\{d\},7\\mathrm\{d\}\\\}, windown∈\{500,2000,5000\}n\\in\\\{500,2000,5000\\\},θalarm∈\{0\.02,0\.05\}\\theta\_\{\\mathrm\{alarm\}\}\\in\\\{0\.02,0\.05\\\}, 3 seeds\. An anytime\-valid upper confidence sequence \(α\\alpha\-spending Clopper–Pearson, peeking\-safe\) upgrades the audit to a finite\-audit deployment guarantee on the same real stream: established atN≈500N\\approx 500–10001000with audited false\-allow≤0\.021\\leq 0\.021at95%95\\%uniformly overNN, with an establish\-then\-halt fallback rule \(control halt\-rate0, and the bound holds even under the severe injected over\-permissive gate; on a deterministic semi\-synthetic rate jump0\.02→0\.120\.02\\to 0\.12the rule halts9,8819\{,\}881audits past the jump\)\. The cumulative sequence is a lifetime guarantee; the two\-window detector above remains the complementary local change detector\.Question\.Is the observedCCprevalence an artifact of one authored gapδ\\delta?Setting\.The analytic taxonomy re\-generated atδ∈\{0\.02,0\.05,0\.08,0\.15,0\.30\}\\delta\\in\\\{0\.02,0\.05,0\.08,0\.15,0\.30\\\},ε=0\.10\\varepsilon=0\.10fixed, natural sampling, on real IEEE\-CIS and NAB \(33seeds\)\.Result\.Pr⁡\[C\]\\Pr\[C\]tracksmin⁡\(δ,ε\)\\min\(\\delta,\\varepsilon\)and saturates aboveε\\varepsilon, and the exact certificate is sound at everyδ\\delta: the geometry predicts the prevalence \(Table[S44](https://arxiv.org/html/2607.29190#A5.T44)\)\.

Table S44:δ\\delta\-sensitivity ofCCprevalence \(EXP\-B1; Section 6\.2\)\. Analytic taxonomy atδ∈\{0\.02,0\.05,0\.08,0\.15,0\.30\}\\delta\\in\\\{0\.02,0\.05,0\.08,0\.15,0\.30\\\},ε=0\.10\\varepsilon=0\.10fixed, natural sampling, 3 seeds, on real IEEE\-CIS \(n≈295n\\approx 295k\) and NAB \(n≈29n\\approx 29k\)\.Pr⁡\[C\]\\Pr\[C\]tracksmin⁡\(δ,ε\)\\min\(\\delta,\\varepsilon\)and saturates aboveε\\varepsilon; the exact certificate hascert\_false\_allow=0\\texttt\{cert\\\_false\\\_allow\}=0at everyδ\\delta\. Levels are dataset\-specific \(boundary density\); themin⁡\(δ,ε\)\\min\(\\delta,\\varepsilon\)*shape*is the claim\.Question\.Was the numeric\-block scaling outcome\-conditioned?Setting\.fscalef\_\{\\mathrm\{scale\}\}selected as the largest sound value on a disjoint SELECTION half and re\-reported on the untouched EVAL half \(grid\{2,3,4,6\}\\\{2,3,4,6\\\},33seeds×2\\times\\,2tracks\)\.Result\.Held\-out selection reproduces the soundness headline: it is not outcome\-conditioned hyperparameter selection \(Table[S45](https://arxiv.org/html/2607.29190#A5.T45)\)\.

Table S45:Held\-outfscalef\_\{\\mathrm\{scale\}\}selection \(EXP\-C4; selection hygiene for the numeric\-block scaling of Tables[S2](https://arxiv.org/html/2607.29190#A5.T2)and[S29](https://arxiv.org/html/2607.29190#A5.T29)\)\.fscalef\_\{\\mathrm\{scale\}\}chosen as the largest value withcert\_false\_allow=0\\texttt\{cert\\\_false\\\_allow\}=0on a disjoint SELECTION half, re\-reported on the untouched EVAL half \(grid\{2,3,4,6\}\\\{2,3,4,6\\\}, 3 seeds×\\times2 tracks\): the soundness headline is not outcome\-conditioned\. The rule genuinely binds on the synthetic track \(dropsfscale=2\.0f\_\{\\mathrm\{scale\}\}=2\.0at selectioncfa=0\.1\\texttt\{cfa\}=0\.1, seed 0\): a smallfscalef\_\{\\mathrm\{scale\}\}under\-resolves the numeric block, so the gate misfits the boundary and its certified allows inherit the misfit\. On NAB the same protocol selects6\.06\.0\(all seeds\) with evalcert\_false\_allow=0\\texttt\{cert\\\_false\\\_allow\}=0andRallow=1\.0R\_\{\\mathrm\{allow\}\}=1\.0: soundness generalizes across the split with no cliff\.Question\.Where does the regime of validity end in the continuous dimension?Setting\.A dimension sweep of the smoothed gate against the true oracle up tok=100k=100\.Result\.Sound and non\-vacuous throughk=50k=50; atk=100k=100the small smoothed gate stops tracking the oracle and the certificate faithfully certifies a weaker gate — gate fidelity, not the certificate, is the bottleneck, and projection removes the edge \(Table[S46](https://arxiv.org/html/2607.29190#A5.T46)\)\.

Table S46:Dimension sweep \(Experiment D\.2; anchors thek=100k=100fidelity edge\)\. Throughk=50k=50the certificate is sound and non\-vacuous; atk=100k=100the small smoothed gate stops tracking the oracle and the certificate faithfully certifies a weaker gate: gate fidelity, not the certificate, is the bottleneck\. Policy\-state projection removes this edge \(Table[S40](https://arxiv.org/html/2607.29190#A5.T40)\)\.Question\.Does randomized\-smoothing confidence survive a deployment horizon?Setting\.CertifiedRallowR\_\{\\mathrm\{allow\}\}versus horizonTTunder a lifetime failure budgetαtotal=0\.01\\alpha\_\{\\mathrm\{total\}\}=0\.01\(EXP\-CX2\)\.Result\.The frozen kill criterion fires: horizon\-corrected RS goes vacuous, so long\-horizon deployments fall back to the deterministic rungs \(Table[S47](https://arxiv.org/html/2607.29190#A5.T47)\)\.

Table S47:Deployment\-horizon confidence for randomized smoothing \(EXP\-CX2; Section 5\.1\)\. CertifiedRallowR\_\{\\mathrm\{allow\}\}on exact robust\-safe records vs horizonTTunder a lifetime failure budgetαtotal=0\.01\\alpha\_\{\\mathrm\{total\}\}=0\.01\(finance track shown; SRE/ops collapse to0sooner\)\. The frozen kill criterion fires: horizon\-corrected RS goes vacuous, per\-recordα\\alphahas a vacuous lifetime bound forT≥103T\\geq 10^\{3\}, adaptive MC buys back utility at44–16×16\\timessampling cost and stays below the deterministic certificate; the11\-Lipschitz backend is horizon\-invariant \(noα\\alpha, no MC; lifetime bound0\)\.Question\.Does the shipped CAGE\-Exact implementation match Definition 1 and Proposition 7?Setting\.A frozen\-seed differential battery:200200fragment policies×1000\\times\\,1000returns \(200,000200\{,\}000total\) against the independent OPA 1\.17\.1 engine evaluated at the exact per\-constraint worst points, plus soundness\-only ball sampling\.Result\.The battery validates the implementation against the independent engine \(Table[S48](https://arxiv.org/html/2607.29190#A5.T48)\)\.

Table S48:Differential validation of CAGE\-Exact \(EXP\-CX3; the empirical leg of Definition 1 / Proposition 7\)\. Frozen\-seed battery:200200fragment policies×1000\\times\\,1000returns \(200,000200\{,\}000total; branches22–66,m≤12m\\leq 12,k≤8k\\leq 8\) against the independent OPA 1\.17\.1 engine evaluated at the exact per\-constraint worst pointsx\+ε​w/‖w‖2x\+\\varepsilon w/\\\|w\\\|\_\{2\}, plus soundness\-only ball sampling and dense grids \(k≤2k\\leq 2\);2020out\-of\-fragment policies must be refused; the sub\-μ\\mus figure of Table S42 is the compiled scalar\-threshold case\.Question\.What autonomy does certification buy at operational operating points?Setting\.Implicit\-isFraudtriage on held\-out mixed traffic \(n=3000n=3000,6868fraud,33seeds\), then the unconditional natural\-traffic accounting \(certified autonomy=Pr⁡\[R\]⋅Rallow=\\Pr\[R\]\\cdot R\_\{\\mathrm\{allow\}\}\)\.Result\.The certified strict\-0frontier admits zero fraud on every seed; the operating points of the Takeaway \(autonomy vs\. in\-budget fraud\) come from these rows, and the exact rung’s natural\-traffic clearance is restated unconditionally \(Tables[S49](https://arxiv.org/html/2607.29190#A5.T49)–[S50](https://arxiv.org/html/2607.29190#A5.T50)\)\.

Table S49:Operational triage \(Section 6\.4\):RallowR\_\{\\mathrm\{allow\}\}as a certified\-autonomy fraction on real IEEE\-CIS \(implicitisFraudpolicy, held\-out mixed trafficn=3000n=3000,6868fraud,33seeds\)\. “In\-budget fraud” is the fraud fraction admitted in the autonomous tranche under theBd,εB\_\{d,\\varepsilon\}attack; the certified strict\-0frontier admits\[0,0,0\]\[0,0,0\]per seed\. Matching the certified volume without the robust\-safe contract re\-opens the exploit\.Table S50:Natural\-traffic autonomy accounting \(Experiment M2; Section 6\.4\)\.RallowR\_\{\\mathrm\{allow\}\}is conditional on the robust\-safe setRR; this table restates it unconditionally on natural traffic: certified autonomy=Pr⁡\[R\]⋅Rallow=\\Pr\[R\]\\cdot R\_\{\\mathrm\{allow\}\}, human\-review volume its complement, natural hazardPr⁡\[C\]\\Pr\[C\]alongside \(δ=0\.08\\delta=0\.08,ε=0\.10\\varepsilon=0\.10\)\. The exact rung\-1 certificate on real data clears about half of all decisions autonomously; the learned rungs at the strict operating point \(ε/σ=1\\varepsilon/\\sigma=1\) trade autonomy for a black\-box\-gate certificate, and that trade\-off is now explicit per setting\.Question\.What do the reported zeros mean statistically?Setting\.Every zero cell quoted in the main tables audited with explicitn/Nn/Nand a Wilson\-95% upper bound, Clopper–Pearson cross\-checked \(9191cells\)\.Result\.All audited cells havek=0k=0with honestly wide intervals whereNNis small, and each row carries an explicit denominator semantics \(Table[S51](https://arxiv.org/html/2607.29190#A5.T51)\)\.

Table S51:Zero\-cell audit \(Experiment M1\): explicitn/Nn/Nand Wilson\-95% upper bound for the zeros quoted in the main tables;9191cells audited, allk=0k=0, Clopper–Pearson cross\-check agreeing throughout\. Small\-NNcells are shown with their honestly wide intervals rather than a bare zero; each row carries an explicit denominator semantics \(certified allows, Category\-CC/UUrecords, exploit witnesses, episodes\)\. Representative rows below; the full 91\-cell audit ships with the code release\.