What Can Be Enforced? A Theory of Certified Runtime Safety for Tool-Using Agents
Shawn Ray
Rigorous, timely theoretical framework for an emerging empirically-dominated field, with a genuinely useful regime taxonomy and evaluation contract, but impact is bounded by its synthesis-over-breakthrough character and extreme density.
Abstract
Runtime guardrails act before irreversible tool calls, but their guarantees depend on what policy state is representable, what a judge observes, and whether intervention changes future behavior. We separate three questions. First, relative to fixed oracle predicates, a deterministic gate enforces exactly the nonempty safety policies whose good prefixes its register model recognizes; policy nontriviality is undecidable with two decrementable counters but in PSPACE for a separable monotone fragment. Second, under a fixed exogenous law, Neyman-Pearson gives the exact false-block/miss frontier and conformal calibration gives a finite-sample marginal certificate, possibly via block-all. Third, once blocking changes future proposals, static scores and ungated trajectories need not identify the closed-loop frontier; a specified finite controlled model instead yields an occupancy program. Bounded representation attacks add a robustness margin, so benign calibration alone does not transfer. Experiments target these distinctions through static diagnostics, controlled-model enumeration, representation rewrites, and paired closed-loop reruns.
AI Impact Assessments
(1 models)Scientific Impact Assessment
Core Contribution
This paper offers a theoretical characterization of *what safety policies runtime guardrails for tool-using LLM agents can enforce, and at what utility cost*. Its central move is to separate three distinct mathematical regimes that prior empirical guardrail work conflates: (1) oracle enforceability — deterministic pre-execution gates enforce exactly the nonempty safety policies whose good prefixes are recognizable by a keyed-counter register automaton, strictly below edit automata; (2) statistical/sequential boundaries — Neyman–Pearson gives the exact one-step false-block/miss frontier, but once blocking alters future proposals, a closed-loop occupancy program (CPOMDP) governs the achievable frontier, which static scores and ungated trajectories provably cannot identify; and (3) calibration/adversarial boundaries — conformal risk control yields a finite-sample marginal certificate (possibly vacuous "block-all"), and bounded representation attacks require a robustness margin so benign calibration does not transfer. The explicitly claimed delta is the *regime-correct composition* of classical results for irreversible semantic gates, plus two genuinely new pieces: feedback non-identifiability (Prop. 2 / Cor. 2) and an analyzable keyed-counter fragment with exact cap-saturation.
Methodological Rigor
The methodological design is a standout strength. The author is unusually disciplined about scope: each theorem states its oracle/stochastic/sequential/adversarial regime, and the paper repeatedly refuses to over-claim (e.g., "certified" is explicitly defined narrowly; sharpness constructions are labeled as not universal lower bounds). Proofs are provided in an appendix and rest on well-established machinery (safety-as-closure, Neyman–Pearson, LP duality for CPOMDPs, Minsky-machine reduction). The empirical work is statistically careful to a degree rarely seen: DeLong correlated-AUC inference, max-T simultaneous intervals, Holm correction, Cochran–Mantel–Haenszel stratification (guarding against a Simpson's-paradox artifact), and McNemar paired tests. Negative controls (0.5B judge at concordance .500) and explicit reporting of vacuous block-all thresholds demonstrate mature experimental hygiene. The main gap: T1 and T3 are only "constructively instantiated," not empirically validated, and the experiments are diagnostic rather than confirmatory of the full theory.
Potential Impact
The most likely durable contributions are the regime taxonomy and the "evaluation contract" / reporting standard (report full ROC not AUC, name the information variable, disclose feedback with paired reruns, state exchangeability and adversarial margin). These are directly usable by the fast-growing agent-guardrail community, which currently reports heterogeneous, hard-to-compare empirical violation rates. The mapping of ~10 existing systems (AgentSpec, ProbGuard, CaMeL, Progent, ShieldAgent, etc.) into these regimes is a valuable orienting device. The finding that AUC cannot be inverted into a deployment requirement, and that calibration is not a security boundary, could meaningfully change practice. Practical adoption is tempered by the heavy conservatism (the effective 3B gate blocks 78% of calls) and by the strong assumptions (finite abstraction, label-conditional exchangeability) needed for the certificates.
Timeliness & Relevance
Extremely timely. Tool-using agents that send email, move money, and call APIs are proliferating, and guardrails are mostly built as ad hoc mechanisms. A foundational "what can be enforced" treatment fills a genuine gap and connects the LLM-safety community to the mature runtime-verification, selective-classification, and constrained-POMDP literatures.
Strengths & Limitations
Strengths: honest, well-scoped theorems; exceptional statistical rigor and reproducibility (public code, cached scores, seeds, prompts, one-command reproduction); genuinely useful synthesis bridging separate fields; the feedback non-identifiability result is a clean, important negative result; the empirical corroboration that text-safety classifiers (Llama-Guard-3) do not transfer to tool-call safety is practically consequential.
Limitations: The novelty is predominantly in composition and framing rather than new mathematics — the two-counter undecidability, Neyman–Pearson optimality, and CPOMDP occupancy LPs are all imported. The paper is extraordinarily dense and compressed; readability suffers substantially, which will limit uptake beyond specialists. It is single-authored and (per the metadata) under review, so community validation is pending. The theory's utility hinges on assumptions (known finite abstraction, exchangeability) that are hard to verify in real deployments, and the experiments show the certificates often collapse to block-all at realistic calibration-set sizes.
Additional Observations
The paper's greatest scientific value may be as a *conceptual reference* that reframes an empirical subfield — comparable to how Schneider's "Enforceable Security Policies" and Ligatti's edit automata anchored classical runtime enforcement. Whether it becomes such an anchor depends on whether the community adopts its regime language. The resource barrier to engaging is low (inference-only, consumer GPUs), which favors extension. The refutation content is real but modest: it qualifies the widespread implicit belief that ROC/AUC characterizes guardrail quality and that calibrated monitors are secure, without overturning a single named load-bearing result.
Overall, this is a rigorous, timely, well-executed theoretical synthesis with a plausible path to influencing evaluation practice, but with impact bounded by presentation density, its synthesis (vs. breakthrough) character, and single-author, pre-validation status.
Generated Jul 28, 2026
Comparison History (22)
Paper 1 has higher potential impact due to its stronger novelty and rigor: it offers a formal theory of what runtime guardrails can enforce (with decidability/complexity results), derives optimal error tradeoffs and finite-sample certificates, and crucially analyzes closed-loop effects where interventions change future agent behavior—central to real deployments. Its framework is broadly applicable to tool-using agents, safety verification, and control/ML, with clear real-world relevance and timeliness. Paper 2 is insightful and practical for evaluation, but is more benchmark/phenomenology-oriented and narrower in methodological depth and generality.
Paper 2 addresses a highly timely and impactful problem: evaluating LLM agents in real physical-world scientific tasks via a robotic chemistry lab with substantial empirical scale (4,608 trials). It offers concrete, actionable diagnostics for deployment readiness and autonomous research, with broad relevance across AI and experimental science. Paper 1 presents rigorous but abstract theoretical results on runtime safety guarantees, valuable but narrower in immediate applicability and accessibility. Paper 2's combination of novelty, empirical rigor, and clear real-world implications gives it higher potential impact.
Paper 2 offers a foundational framework establishing the mathematical and computational limits of runtime guardrails for AI agents. By connecting agent safety to computability theory (undecidability, PSPACE) and statistical guarantees, it provides enduring theoretical bounds. While Paper 1 introduces a highly relevant practical model for evolving agent authorization, Paper 2's rigorous formalization of what is fundamentally enforceable will likely serve as a foundational limits-of-enforcement text, driving broader, long-lasting scientific impact across AI safety and formal verification.
Paper 2 has higher potential scientific impact because it establishes foundational, theoretical guarantees for AI agent safety, a universally critical challenge. By formalizing certified runtime guardrails, undecidability boundaries, and conformal calibration for tool-using agents, it offers broad, rigorous contributions to AI safety and theoretical computer science. In contrast, Paper 1 presents an applied, empirical evaluation of existing LLMs for a specific software engineering task. While practically useful, Paper 1 offers narrower scientific innovation and lacks the cross-disciplinary, foundational impact of Paper 2.
Paper 2 likely has higher scientific impact: it introduces a timely, high-stakes benchmark at the AI–biosecurity interface with direct real-world applicability (measuring dual-use capabilities) and includes wet-lab validation, increasing credibility and uptake potential. Benchmarks often become community standards, influencing policy, evaluation practices, and model development across AI safety, biosecurity, and ML. Paper 1 is more theoretically novel and rigorous for runtime enforcement, but its impact may be narrower and more contingent on adoption in specific tool-using agent stacks, whereas ABC-Bench addresses an urgent cross-field need with immediate operational relevance.
Paper 1 offers a novel theoretical framework for certified runtime safety in tool-using agents, addressing fundamental questions of enforceability, statistical detection frontiers, and closed-loop dynamics with rigorous formal results (decidability, PSPACE, Neyman-Pearson, conformal calibration). This provides lasting conceptual foundations applicable across agent safety research. Paper 2 is a valuable empirical benchmark but is inherently more incremental and tied to a specific task set that may become dated quickly. The theoretical depth and broad applicability of Paper 1 suggest higher and more durable scientific impact in the critical, timely area of agent safety.
Paper 1 addresses a highly timely and critical issue (AI agent safety) with a novel, rigorous theoretical framework combining formal methods and statistical guarantees. Its implications for deploying secure, autonomous tool-using agents give it broader, more immediate real-world and cross-disciplinary impact compared to Paper 2's narrower, albeit effective, algorithmic improvement to classic 2D grid pathfinding.
Paper 2 establishes a foundational theoretical framework for certified runtime safety in tool-using AI agents. While Paper 1 provides a valuable algorithmic improvement for tabular feature engineering, Paper 2 addresses a critical, high-stakes bottleneck in AI deployment: provable guardrails. By defining formal decidability limits, statistical guarantees, and closed-loop dynamics for agent interventions, Paper 2 demonstrates exceptional methodological rigor. Its theoretical contributions are essential for safely deploying autonomous agents, yielding a broader and more profound scientific impact than an applied feature engineering method.
Paper 2 establishes a foundational theoretical framework for certified runtime safety in tool-using AI agents. By proving formal computational boundaries (e.g., undecidability vs. PSPACE) and statistical guarantees for guardrails, it provides rigorous methodological bounds that will outlast current model architectures. While Paper 1 presents a practical and highly timely approach to multimodal misinformation detection, Paper 2's rigorous mathematical approach to fundamental AI safety challenges gives it a significantly higher potential for long-lasting, cross-disciplinary scientific impact in the rapidly growing field of autonomous agents.
Paper 2 has higher potential impact due to greater novelty and breadth: it develops a general theory of what runtime guardrails can certify for tool-using agents, spanning computability/complexity limits, statistical tradeoffs (Neyman–Pearson, conformal certificates), and closed-loop control effects. These results are broadly applicable across AI safety, agents, verification, and ML evaluation, and are highly timely given rapid deployment of tool-using LLM systems. Paper 1 is methodologically strong with real-world ad gains, but is more domain-specific (creative optimization) and mainly an engineering workflow extension rather than a foundational advance.
Rigorous, timely theoretical framework for an emerging empirically-dominated field, with a genuinely useful regime taxonomy and evaluation contract, but impact is bounded by its synthesis-over-breakthrough character and extreme density.