# Containment Verification: AI Safety Guarantees Independent of Alignment

arXiv: https://arxiv.org/abs/2605.09045 · HTML: https://mlsanity.com/paper/2605.09045/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Agent threats, guardrails and governance, one of 16 directions in LLM agents and tool use.
- Builds on 12 of its 30 references that are in the map.
- First posted on arXiv 9 May 2026.

## Placed in

- LLM agents and tool use / [Agent threats, guardrails and governance](https://mlsanity.com/agents/agent-threats-guardrails-and-governance/)

## Builds on (most cited first, 12 of 12)

- [Language Models Don't Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Prompting](https://mlsanity.com/paper/2305.04388/) (2023)
- [Open Problems and Fundamental Limitations of Reinforcement Learning from Human Feedback](https://mlsanity.com/paper/2307.15217/) (2023)
- [Measuring Faithfulness in Chain-of-Thought Reasoning](https://mlsanity.com/paper/2307.13702/) (2023)
- [Sleeper Agents: Training Deceptive LLMs that Persist Through Safety Training](https://mlsanity.com/paper/2401.05566/) (2024)
- [The Alignment Problem from a Deep Learning Perspective](https://mlsanity.com/paper/2209.00626/) (2022)
- [AI Control: Improving Safety Despite Intentional Subversion](https://mlsanity.com/paper/2312.06942/) (2023)
- [Is Power-Seeking AI an Existential Risk?](https://mlsanity.com/paper/2206.13353/) (2022)
- [VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation](https://mlsanity.com/paper/2510.05156/) (2025)
- [Dafny as Verification-Aware Intermediate Language for Code Generation](https://mlsanity.com/paper/2501.06283/) (2025)
- [ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis](https://mlsanity.com/paper/2512.10173/) (2025)
- [How Catastrophic is Your LLM? Certifying Risk in Conversation](https://mlsanity.com/paper/2510.03969/) (2025)
- [Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability](https://mlsanity.com/paper/2604.00280/) (2026)

## Built on by (most cited first, 1 of 1)

- [Individual Disempowerment through an Advice Channel: Control Loss when Influence is Endogenous](https://mlsanity.com/paper/2608.14795/) (2026)

## Abstract (arXiv)

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 over the framework's typed action space, and the verified containment layer must enforce the boundary policy for every typed action value the AI can emit. 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. The guarantee is independent of alignment because it quantifies over the framework's typed action boundary rather than over model behavior.