Containment Verification: AI Safety Guarantees Independent of Alignment
Royce Moon, Lav R. Varshney
Abstract
Agentic frameworks are the software layer through which AI agents act in the world. Existing safety methods intervene on the model and therefore remain conditional on unverifiable properties of learned behavior. We introduce containment verification, which locates safety guarantees in the agentic framework itself. Under havoc oracle semantics, the AI is modeled as an unconstrained oracle ranging over the entire typed action space, and the verified containment layer must enforce the boundary policy for every possible AI output. For boundary-enforceable properties, expressed over modeled boundary events, action arguments, and state, we prove a universal guarantee by forward-simulation refinement and mechanize it in Dafny. We instantiate the paradigm by verifying PocketFlow, a minimalist agentic LLM framework, and use an agentic synthesis pipeline to generate the specification, operational model, and refinement proof under an information barrier against tautological specifications. To our knowledge, this is the first deductive formal verification of an agentic framework, and its guarantee is invariant to model capability over the modeled typed action boundary.
AI Impact Assessments
(1 models)Scientific Impact Assessment: Containment Verification
Core Contribution
The paper introduces *containment verification*, a paradigm that locates AI safety guarantees in the agentic framework layer rather than in the AI model itself. The key insight is treating the AI as a "havoc oracle"—an unconstrained procedure that can return any value of its typed action space—and then proving that the surrounding containment layer enforces boundary safety policies regardless of what the oracle emits. This is formalized via forward-simulation refinement between an abstract safety specification and a concrete operational model, mechanized in Dafny.
The conceptual contribution is genuinely novel in framing: rather than verifying the AI (which is intractable for learned systems), verify the deterministic software that mediates between the AI and the world. The analogy to physical fail-safes (gravity-dropped control rods, pressure relief valves, hardware memory protection) is apt and well-articulated.
Methodological Rigor
Formal framework: The theoretical apparatus—labeled transition systems, havoc oracle semantics, boundary-event refinement (Definition 3.1), and the soundness theorem (Theorem 3.2)—is cleanly presented and mathematically sound. The proof structure follows the well-established IronFleet idiom, lending credibility. The theorem is straightforward once the definitions are set up: it's essentially a standard forward-simulation argument with labeled events.
Mechanization: The Dafny mechanization is a genuine strength. Machine-checked proofs eliminate the possibility of subtle proof errors. The artifact excerpts in the appendix demonstrate concrete refinement obligations, safety predicates, and the soundness lemma.
Instantiation concerns: However, the instantiation is notably thin. PocketFlow is described as a "minimalist" framework with only a four-variant action type (NoAction, ReadPathAction, ToolCallAction, StepAction). The safety properties verified are correspondingly simple: workspace-rooted reads, allowlisted tool calls, and bounded step counts. While these serve as proof-of-concept, they are far from the complexity of real production deployments.
Synthesis pipeline: The seven-phase agentic pipeline for generating specifications is interesting but raises circularity concerns. Using LLMs (Claude Sonnet/Opus) to synthesize formal specifications for an LLM framework is conceptually clean only because the Dafny verifier serves as the ultimate arbiter. The information barrier against tautological specifications is a thoughtful design choice, though the paper honestly acknowledges its limitations—the silent abstention problem (Section 4.6) where the no-barrier mode produces vacuously true predicates that pass all three validation gates.
Three-gate validation: The vacuity and discrimination gates adapt existing ideas (from temporal model checking and IronSpec) but are shown to be insufficient—they don't catch property-completeness gaps. This honest admission is valuable but also reveals a significant methodological gap.
Potential Impact
Conceptual impact: The paper's strongest contribution is conceptual. The taxonomy in Table 1 (organizing safety approaches by locus and guarantee strength) provides a useful framework for thinking about AI safety. The distinction between oracle-level and container-level safety mechanisms, and the argument that only container-level approaches can achieve universal guarantees, is compelling within its stated scope.
Practical impact: Currently limited. The gap between verifying a four-variant action type on PocketFlow and verifying production frameworks like LangChain (with dozens of tools, complex state management, and rich dispatch logic) is enormous. The paper acknowledges this ("the engineering test of the paradigm is whether it scales"), but the scaling path remains undemonstrated.
Impact on adjacent fields: The havoc oracle semantics approach could influence how other safety-critical software systems are verified when they incorporate ML components. The paradigm generalizes beyond AI agents to any system where an unpredictable component operates within a deterministic mediation layer.
Timeliness & Relevance
The paper is timely. As AI agents are deployed in increasingly consequential settings (financial systems, code execution, autonomous operations), the need for formal safety guarantees is acute. The paper correctly identifies that alignment-based approaches face fundamental verifiability challenges that worsen with capability scaling. The framing that containment verification's assumptions scale with engineering effort rather than model capability is the paper's most important conceptual contribution.
Strengths
1. Clean conceptual framework that reframes AI safety from model properties to infrastructure properties
2. Machine-checked proofs in Dafny, following established verification methodology
3. Honest limitations section that clearly delineates what the approach does and does not cover
4. Effect exclusivity is clearly stated as an assumption rather than hidden
5. Capability invariance argument is logically sound—the guarantee genuinely doesn't weaken with model capability over the modeled boundary
Limitations
1. Narrow instantiation: A four-variant action type on a minimalist framework is far from demonstrating practical viability. The paper's central engineering claim—that formal verification of containment layers is feasible—remains weakly supported.
2. Effect exclusivity is extremely strong: In practice, agents may have side channels, access to `eval`-like primitives, or interact with the world through paths not mediated by the typed action interface. The paper acknowledges this but the assumption substantially narrows real-world applicability.
3. Specification completeness is unresolved: The paper demonstrates that its own validation gates fail to catch vacuously true specifications (the silent abstention problem). This means the guarantee's practical strength depends on manual audit of specification quality—partially undermining the automation claims.
4. Content-level exclusion: By design, the approach cannot address truthfulness, deception, manipulation, or persuasion—arguably the most pressing near-term AI safety concerns. The paper is upfront about this, but it limits the paradigm's coverage.
5. No comparison with runtime monitoring: Systems like AgentSpec and CaMeL provide runtime enforcement with lower verification burden. A comparative analysis of the guarantee-strength vs. engineering-cost tradeoff would strengthen the practical argument.
6. Scalability undemonstrated: The jump from PocketFlow to production frameworks is acknowledged but not addressed beyond future-work aspirations.
Overall Assessment
This is a well-crafted conceptual contribution that establishes a formal foundation for infrastructure-level AI safety guarantees. The theoretical framework is sound, the mechanization is genuine, and the limitations are honestly presented. However, the practical instantiation is too narrow to validate the paradigm's feasibility at scale, and the specification synthesis pipeline reveals unresolved quality assurance challenges. The paper's lasting impact will likely be conceptual—providing a vocabulary and framework for thinking about where safety guarantees should be located—rather than immediately practical.
Generated May 12, 2026
Comparison History (25)
Paper 1 presents a foundation model trained on an unprecedented scale of wearable data (5 million participants) with immediate, broad applications across 35 diverse health tasks. Its integration of LLMs for few-shot learning and clinician-validated personalized health agents offers massive, tangible real-world impact in healthcare and personalized medicine, slightly edging out the important but more specialized theoretical contributions of Paper 2 in formal AI safety verification.
Paper 2 introduces a fundamentally new paradigm for AI safety—containment verification—that provides formal, model-independent safety guarantees for agentic AI systems. This is a foundational contribution with broad implications across AI safety, formal methods, and software verification, addressing one of the most critical challenges as AI agents become more capable. While Paper 1 is impressive applied work demonstrating LLM-guided automated forecasting, it represents an incremental advance in automation of existing epidemiological methods. Paper 2's theoretical framework and formal verification approach could reshape how the entire field approaches AI safety, giving it broader and deeper long-term impact.
Paper 2 is likely to have higher scientific impact due to broader, immediate utility: a large, open, evolving Lean 4 benchmark with open conjectures enables standardized evaluation, drives community contributions, and directly supports verified mathematical discovery. Its applications span automated reasoning, theorem proving, benchmarking, and AI evaluation, with demonstrated real-world impact via resolved conjectures. Paper 1 is highly novel and rigorous (deductive verification for agentic frameworks under worst-case semantics) with important AI safety implications, but its impact may be narrower near-term (boundary-enforceable properties, specific framework assumptions) and adoption depends on integration into widely used agent stacks.
Paper 2 is more novel and foundational: it shifts safety guarantees from opaque model behavior to formally verified agentic frameworks with universal (havoc-oracle) semantics, yielding capability-invariant guarantees. The methodological rigor is higher via mechanized proofs in Dafny and a concrete verified framework (PocketFlow), and its ideas can generalize across many AI systems that use tool/action interfaces, impacting formal methods, security, and AI safety. Paper 1 has strong real-world applicability and timeliness, but its impact is more operational and contingent on ecosystem adoption and evaluation design, with fewer transferable scientific guarantees.
Paper 1 pioneers a highly novel approach to AI safety by formally verifying the agentic framework rather than the model itself. This alignment-independent guarantee addresses a critical bottleneck in deploying autonomous agents safely. While Paper 2 offers a strong self-improvement method for LLMs, Paper 1's use of deductive formal verification for AI containment presents a paradigm shift with profound implications for verifiable AI safety, offering broader and more foundational scientific impact.
Paper 1 addresses a critical, high-stakes bottleneck in AI deployment by introducing a novel, verifiable approach to AI safety for agentic frameworks. Its guarantee of safety independent of model alignment offers immense real-world applicability and broad impact across any domain deploying autonomous agents. While Paper 2 provides a valuable benchmark for advanced mathematical reasoning, its impact is largely confined to the autoformalization subfield, making Paper 1 significantly more impactful overall.
Paper 2 is more likely to have higher scientific impact due to its conceptual novelty (shifting safety guarantees from model behavior to formally verified agentic frameworks) and broad, timely relevance to AI safety. It introduces a general verification paradigm (havoc oracle semantics, boundary-enforceable properties) with mechanized proofs in Dafny and a concrete verified framework (PocketFlow), enabling rigorous, capability-invariant guarantees. This could influence multiple areas—formal methods, security, agent frameworks, and governance—whereas Paper 1, though strong and application-validated, is a narrower methodology improvement within LLM-assisted scientific ideation.
Paper 1 is more novel and potentially high-impact: it shifts AI safety guarantees from model-dependent alignment to formally verified agentic frameworks under adversarial (havoc oracle) semantics, with mechanized proofs in Dafny. This offers strong, capability-invariant safety guarantees and a reusable methodology that can influence AI safety, formal methods, and systems engineering. Paper 2 is timely and useful (a multi-task MARL foundation model), but is closer to scaling existing offline RL/transformer paradigms with large datasets; impact may be narrower and more incremental, and methodological rigor hinges on empirical benchmarks rather than provable guarantees.
Paper 2 introduces a fundamentally new paradigm for AI safety—containment verification—that provides formal guarantees independent of model alignment, addressing a critical and broadly relevant challenge as agentic AI systems proliferate. The theoretical contribution (havoc oracle semantics, forward-simulation refinement, mechanized proofs in Dafny) is novel and rigorous, with potential impact across AI safety, formal methods, and software engineering. Paper 1, while practically useful for scientific data processing, represents more incremental progress in LLM-based automation. Paper 2's breadth of impact and timeliness regarding AI safety concerns give it the edge.
Paper 2 likely has higher impact due to its strong novelty (formal, model-agnostic safety guarantees via containment verification), methodological rigor (deductive verification with mechanized proofs in Dafny), and broad cross-field relevance (AI safety, formal methods, programming languages, agentic systems). Its real-world applicability is direct: verifiable containment layers for agentic frameworks are actionable for deployment. Paper 1 offers interesting interpretability/architecture insights for LVLMs, but the claim that attention can be replaced with noise may be brittle and narrower in scope; impact is more confined to ML model analysis/optimization.
Paper 1 addresses a critical and highly timely challenge in AI safety: constraining autonomous agents. By decoupling safety guarantees from model alignment and using formal verification on the agentic framework, it introduces a highly novel, mathematically rigorous paradigm. This structural approach to AI containment has immense potential to become a foundational practice in deploying safe AI systems, offering broader transformational impact compared to Paper 2's theoretical unification of fairness and explainability, though both are important.
Paper 2 has higher potential impact due to its novelty and breadth: it reframes AI safety guarantees as properties of the agentic framework, verified under havoc-oracle semantics, yielding alignment-independent, capability-invariant guarantees within a typed action boundary. The use of mechanized deductive verification (Dafny) and a non-tautological spec-generation pipeline suggests strong methodological rigor and a foundation that can generalize across domains (formal methods, security, AI safety, agent frameworks). Paper 1 is timely and practically useful, but is narrower and model/benchmark-specific.
Paper 1 introduces a fundamentally new paradigm for AI safety—containment verification—that provides formal safety guarantees independent of model alignment, a novel and critically important contribution. It presents the first deductive formal verification of an agentic framework with mechanized proofs, addressing a foundational problem as AI capabilities scale. Its cross-cutting relevance to AI safety, formal methods, and software engineering gives it broad impact potential. Paper 2, while solid engineering work improving agentic orchestration with flow-matching, represents a more incremental advance in LLM agent optimization with narrower conceptual novelty.
Paper 2 introduces a fundamentally novel paradigm for AI safety—containment verification—that provides formal guarantees independent of model alignment or capability level. This is a significant conceptual advance: shifting safety from unverifiable model properties to verifiable framework properties. It includes mechanized proofs in Dafny and claims to be the first deductive formal verification of an agentic framework. Given the urgency of AI safety, its broad applicability across all agentic AI systems, and the growing deployment of AI agents, this work has high potential for cross-disciplinary impact in AI safety, formal methods, and software engineering. Paper 1, while insightful for interpretability, is more incremental.
Paper 1 is more novel and potentially higher-impact: it proposes a new safety paradigm (containment guarantees independent of model alignment) and demonstrates mechanized deductive verification of an agentic framework under adversarial “havoc oracle” semantics—methodologically rigorous and broadly relevant across AI safety, formal methods, and agent frameworks. If adopted, it could influence how safety-critical agent boundaries are engineered and certified. Paper 2 is timely and useful as an evaluation resource for scientific-agent capabilities, but benchmarks typically have narrower, domain-specific impact and less foundational innovation than a general verification methodology.
Paper 1 introduces a fundamentally new paradigm for AI safety—shifting guarantees from model alignment to the agentic framework layer—with formal verification providing mathematically provable safety properties independent of model capability. Given the urgency and scale of AI safety concerns, the timeliness is exceptional. The approach is methodologically rigorous (mechanized proofs in Dafny) and broadly applicable to any agentic AI system. Paper 2 offers interesting but incremental insights into cultural transmission via RL simulations, contributing to a more niche intersection of cognitive science and social learning with narrower real-world applicability.
Paper 2 addresses a critical, foundational problem in AI safety by proposing a model-agnostic, formal verification approach for agentic frameworks. Its methodological rigor (mechanized proofs in Dafny) and broad applicability across any AI deployment give it significantly higher potential impact compared to Paper 1, which, while valuable, focuses on a specific, narrow application (storytelling for older adults).
Paper 1 addresses the critical and urgent issue of AI safety by introducing a formally verified containment layer, offering mathematical guarantees independent of model alignment. This foundational shift provides a highly rigorous, novel paradigm with profound implications across all AI deployments. In contrast, Paper 2 offers valuable but incremental architectural improvements to LLM memory, an active but narrower field, making Paper 1 more impactful.
Paper 1 addresses a critical and highly urgent problem in AI safety by providing mathematically proven containment guarantees for AI agents, independent of the model's internal alignment. Its novel intersection of formal verification and agentic frameworks offers broad, real-world applicability for deploying safe AI systems. Paper 2 is a valuable cognitive science study on human learning, but Paper 1's methodological rigor and direct relevance to mitigating existential AI risks give it a significantly higher potential for broad scientific and societal impact.
Paper 2 introduces a fundamentally novel paradigm—containment verification—that provides AI safety guarantees independent of model alignment, addressing a critical unsolved problem. It offers formal, deductive verification of an agentic framework (a first), with provable universal guarantees. This has enormous implications for AI safety policy, deployment of autonomous agents, and formal methods. Paper 1 is a useful survey organizing graph-LLM integration but synthesizes existing work rather than introducing new methodology. Paper 2's originality, theoretical rigor, and direct relevance to the urgent AI safety challenge give it substantially higher impact potential.