Containment Verification: AI Safety Guarantees Independent of Alignment

TL;DR

This paper introduces a novel containment verification approach that provides AI safety guarantees directly within the agentic framework, independent of the AI model's learned behavior.

Contribution

It presents the first deductive formal verification of an agentic framework, ensuring safety guarantees invariant to model capability.

Findings

Verified containment layer enforces safety boundary for all AI outputs

Formal proof of universal safety guarantee via Dafny mechanization

Demonstrated verification on a minimalist agentic LLM framework

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.