Containment Verification: AI Safety Guarantees Independent of Alignment

• URL: http://arxiv.org/abs/2605.09045v1
• Date: Sat, 09 May 2026 16:36:45 GMT
• Title: Containment Verification: AI Safety Guarantees Independent of Alignment
• Abstract summary: We introduce containment verification, which locates safety guarantees in the agentic framework itself.<n>Under havoc oracle semantics, the AI is modeled as an unconstrained oracle ranging over the entire typed action space.<n>For boundary-enforceable properties, expressed over modeled boundary events, action arguments, and state, we prove a universal guarantee.
• Score: 13.629487815782355
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• Adversarial Attacks in Multi-Agent LLM Pipelines: Unveiling Structural Vulnerabilities in Agentic AI Architectures [4.053243845971823]
  Multi-agent LLM pipelines orchestrate specialized language model agents into structured where intermediate outputs are passed across agents to solve complex tasks.<n>This design introduces a security gap absent in single-agent settings: once an agent accepts adversarial content, it is propagated as trusted input throughout the pipeline.<n>We argue that this vulnerability stems from the absence of boundary verification, a security primitive that enforces explicit validation of data as it crosses inter-agent boundaries.
  arXiv  Detail & Related papers  (2026-08-01T15:35:58Z)
• Operational Hallucination and Safety Drift in AI Agents [0.3823356975862005]
  Large language models (LLMs) serving as planners in tool-using autonomous agents introduce dynamic reliability risks in multi-turn execution.<n>This paper empirically characterizes two observed failure modes across multiple state-of-the-art LLMs: Safety Drift and Operational Hallucination.<n>We propose an Action-Aware Supervision Layer - a lightweight, plug-and-play architectural blueprint incorporating intent-action consistency checks, state tracking, and forced termination primitives.
  arXiv  Detail & Related papers  (2026-07-20T17:01:50Z)
• Provably Secure Agent Guardrail [89.79561918065122]
  Existing defense architectures rely on empirical semantic guardrails and probabilistic large model adjudicators.<n>This paper proposes a new security paradigm for agents based on the fundamental limitations of logical reasoning.
  arXiv  Detail & Related papers  (2026-05-28T02:12:41Z)
• From CRUD to Autonomous Agents: Formal Validation and Zero-Trust Security for Semantic Gateways in AI-Native Enterprise Systems [0.0]
  This paper proposes the design, formal validation, and empirical evaluation of a Semantic Gateway governed by the Model Context Protocol (MCP)<n>The gateway reframes the enterprise API as a semantic surface where tools are dynamically discovered, authorized, and executed based on intent and policy enforcement.<n>The architecture introduces a three-layer Zero-Trust security model comprising a pre-inference Semantic Firewall, deterministic Tool-Level RBAC, and out-of-band Cryptographic Human-in-the-Loop approval.
  arXiv  Detail & Related papers  (2026-04-28T12:25:06Z)
• CORA: Conformal Risk-Controlled Agents for Safeguarded Mobile GUI Automation [68.53387633351484]
  We propose CORA (COnformal Risk-controlled GUI Agent), a post-policy, pre-action safeguarding framework that provides statistical guarantees on harmful executed actions.<n> CORA reformulates safety as selective action execution: we train a Guardian model to estimate action-conditional risk for each proposed step.<n>To rigorously evaluate this paradigm, we introduce Phone-Harm, a new benchmark of mobile safety violations with step-level harm labels.
  arXiv  Detail & Related papers  (2026-04-10T09:41:21Z)
• BarrierSteer: LLM Safety via Learning Barrier Steering [83.12893815611052]
  BarrierSteer is a novel framework that formalizes safety by embedding learned non-linear safety constraints directly into the model's latent representation space.<n>We show that BarrierSteer substantially reduces adversarial success rates, decreases unsafe generations, and outperforms existing methods.
  arXiv  Detail & Related papers  (2026-02-23T18:19:46Z)
• Agentic Problem Frames: A Systematic Approach to Engineering Reliable Domain Agents [0.0]
  Large Language Models (LLMs) are evolving into autonomous agents, yet current "frameless" development--relying on ambiguous natural language--leads to critical risks such as scope creep and open-loop failures.<n>This study proposes Agentic Problem Frames (APF), a systematic engineering framework that shifts focus from internal model intelligence to the structured interaction between the agent and its environment.
  arXiv  Detail & Related papers  (2026-02-22T06:32:32Z)
• Steering Externalities: Benign Activation Steering Unintentionally Increases Jailbreak Risk for Large Language Models [62.16655896700062]
  Activation steering is a technique to enhance the utility of Large Language Models (LLMs)<n>We show that it unintentionally introduces critical and under-explored safety risks.<n>Experiments reveal that these interventions act as a force multiplier, creating new vulnerabilities to jailbreaks and increasing attack success rates to over 80% on standard benchmarks.
  arXiv  Detail & Related papers  (2026-02-03T12:32:35Z)
• GAVEL: Towards rule-based safety through activation monitoring [2.337566423505956]
  Large language models (LLMs) are increasingly paired with activation-based monitoring to detect and prevent harmful behaviors.<n>Existing activation safety approaches, trained on broad misuse datasets, struggle with poor precision, limited flexibility, and lack of interpretability.<n>This paper introduces a new paradigm: rule-based activation safety, inspired by rule-sharing practices in cybersecurity.
  arXiv  Detail & Related papers  (2026-01-27T16:31:39Z)
• CaMeLs Can Use Computers Too: System-level Security for Computer Use Agents [60.98294016925157]
  AI agents are vulnerable to prompt injection attacks, where malicious content hijacks agent behavior to steal credentials or cause financial loss.<n>We introduce Single-Shot Planning for CUAs, where a trusted planner generates a complete execution graph with conditional branches before any observation of potentially malicious content.<n>Although this architectural isolation successfully prevents instruction injections, we show that additional measures are needed to prevent Branch Steering attacks.
  arXiv  Detail & Related papers  (2026-01-14T23:06:35Z)
• Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
  Large language model (LLM)-based AI agents extend capabilities by enabling access to tools such as data sources, APIs, search engines, code sandboxes, and even other agents.<n>LLMs may invoke unintended tool interactions and introduce risks, such as leaking sensitive data or overwriting critical records.<n>Current approaches to mitigate these risks, such as model-based safeguards, enhance agents' reliability but cannot guarantee system safety.
  arXiv  Detail & Related papers  (2026-01-12T21:31:38Z)
• AI Bill of Materials and Beyond: Systematizing Security Assurance through the AI Risk Scanning (AIRS) Framework [31.261980405052938]
  Assurance for artificial intelligence (AI) systems remains fragmented across software supply-chain security, adversarial machine learning, and governance documentation.<n>This paper introduces the AI Risk Scanning (AIRS) Framework, a threat-model-based, evidence-generating framework designed to operationalize AI assurance.
  arXiv  Detail & Related papers  (2025-11-16T16:10:38Z)
• AgentGuard: Runtime Verification of AI Agents [1.14219428942199]
  AgentGuard is a framework for runtime verification of Agentic AI systems.<n>It provides continuous, quantitative assurance through a new paradigm called Dynamic Probabilistic Assurance.
  arXiv  Detail & Related papers  (2025-09-28T13:08:50Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  We introduce a novel problem formulation called Abstract DNN-Verification, which verifies a hierarchical structure of unsafe outputs.<n>By leveraging abstract interpretation and reasoning about output reachable sets, our approach enables assessing multiple safety levels during the formal verification process.<n>Our contributions include a theoretical exploration of the relationship between our novel abstract safety formulation and existing approaches.
  arXiv  Detail & Related papers  (2025-05-08T13:29:46Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.