Source note
Containment Verification: AI Safety Guarantees Independent of Alignment
Summary
Containment verification proves safety properties in the agent runtime instead of relying on the model to behave. The paper verifies PocketFlow in Dafny so every typed AI action must pass a checked boundary policy.
Problem
- Agentic AI systems can trigger external effects such as filesystem reads, tool calls, network access, financial actions, database changes, or infrastructure tampering.
- Model-level safety methods depend on learned behavior, which the paper says cannot be formally verified and can fail in deployment.
- The method matters for boundary failures: if every effect crosses a typed action interface, the runtime can block out-of-policy effects even when the model emits hostile or unexpected actions.
Approach
- The AI is modeled as a havoc oracle: a Dafny external method that can return any value in the typed
Actionspace. - Safety policies are written over action arguments, modeled boundary events, and system state. The claim depends on effect exclusivity: every relevant external effect must pass through the modeled interface.
- The proof uses forward-simulation refinement between an abstract boundary-safety state machine and the concrete PocketFlow operational model.
- The Dafny proof checks that every concrete boundary event matches an abstract safe event, so rejected actions become no-effect events rather than unmodeled behavior.
- An agentic synthesis pipeline generates the specification, operational model, and refinement proof, with an information barrier and validation gates to reduce tautological or vacuous specs.
Results
- Theorem 3.2 claims universal boundary safety: for every trace under any concrete oracle, the concrete policy holds at every step, if abstract havoc safety, boundary-event refinement, and effect exclusivity hold.
- The PocketFlow instantiation uses a typed action interface with 4 variants:
NoAction,ReadPathAction,ToolCallAction, andStepAction. - The verified boundary policy induces 3 recorded invariants: every read path stays under the workspace root, every tool call is allowlisted, and the step counter stays within its bound.
- The proof is mechanized in Dafny and includes named lemmas such as
RefinementInit,RefinementNext, andContainmentVerificationSoundness. - The synthesis process has 7 phases and adds resolution, vacuity, and discrimination gates before iterative Dafny proof repair.
- The excerpt gives no runtime benchmark, throughput result, attack-success rate, or comparison table; its strongest empirical claim is a Dafny-checked PocketFlow verification artifact.