Adnan KhanAdnanProduct & AI
San Francisco Bay Area
Get in touch

Source note3 min read

The Unfireable Safety Kernel: Execution-Time AI Alignment for AI Agents and Other Escapable AI Systems

Source

arXiv

arxiv.org/abs/2606.26057v1

Read the source

Source

Plain-Language Brief

The Unfireable Safety Kernel is a Rust reference implementation of an execution-time AI alignment system designed for escapable AI systems, which are AI agents or other systems with significant influence over their own runtime. The paper presents the four properties that an authorization mechanism must satisfy to provide architectural control and introduces the Unfireable Safety Kernel as a solution meeting these requirements. The kernel was machine-checked using Z3 theorem proving and exhaustive bounded-model checking, and it demonstrated success in controlling a live, escapable AI system against an escape-seeking adversary.

What the Document Says

  • AI agents have access to tools, APIs, and infrastructure.
  • Controls are placed inside the agent's own runtime (system prompts, output filters, guardrail libraries).
  • Any control in the agent's address space is reachable by inputs that influence it.
  • The paper defines 'escapable AI systems' as those with sufficient reach into their own runtime.
  • Four properties are identified for an authorization mechanism to provide architectural control:
    1. Process separation
    1. Pre-action enforcement on a structurally only path
    1. Fail-closed at both the request and system levels
    1. Externalized signed evidence verifiable outside the controlled system's trust boundary
  • The Unfireable Safety Kernel is presented as a Rust reference implementation realizing all four properties.
  • The fail-closed invariant of the kernel was machine-checked using SMT theorem (Z3) and exhaustive bounded-model checking.
  • A Python-to-Rust migration was ensured to maintain byte-equivalence.
  • The paper presents an evaluation of the kernel governing a live, escapable AI system against an escape-seeking adversary, with successful results.
  • Against 3 contemporary systems claiming agent control, the agent lacked the choice in this study.

Key Concepts Mentioned

  • AI alignment
  • escapable AI systems
  • authorization mechanism
  • Unfireable Safety Kernel

Claims Made by the Document

  • The Unfireable Safety Kernel effectively controls a live, escapable AI system.
  • The kernel's design ensures architectural control through four specific properties.

Evidence Used

  • Evaluation of the kernel against an escape-seeking adversary
  • Machine-checking using Z3 theorem proving and exhaustive bounded-model checking

Methods / Approach

UNKNOWN

Limitations Stated by the Authors

UNKNOWN

Limitations Noted by the Agent

Agent interpretation — not from the source.

UNKNOWN

Open Questions

UNKNOWN

Notes for Future Q&A

May include interpretation. Labeled where it does.

UNKNOWN

Raw Abstract / Excerpt

AI agents are granted access to tools, APIs, and other infrastructure, making them active principals in those systems. The dominant approach places controls inside the agent's own runtime: system prompts, output filters, and guardrail libraries. Any control in the agent's address space is reachable by inputs that influence it; this generalizes to any AI system with sufficient reach into its own runtime, a class we term escapable AI systems. We identify four properties that an authorization mechanism must satisfy for architectural control rather than for cooperative requests: process separation, pre-action enforcement on a structurally only path, fail-closed at both the request and system levels, and externalized signed evidence verifiable outside the controlled system's trust boundary. We position this layer as execution-time AI alignment, complementing training-time alignment (RLHF, Constitutional AI) and inference-time alignment. We present the Unfireable Safety Kernel, a Rust reference implementation realizing all four. Its fail-closed invariant is machine-checked at two levels: an SMT theorem (Z3) and an exhaustive bounded-model-checking proof of the production decision function (Kani, 4/4 harnesses). A Python-to-Rust migration was gated on byte-equivalence (1000/1000 fixtures; 17/17 adversarial classes). We evaluate the kernel governing a live, escapable AI system, a deterministic, self-improving world model, against an escape-seeking adversary driving its real self-modification seam: across 1,000 self-modifications, all 704 attempts on the safety-critical core are refused, with no escape; a further 300, under the operator kill switch, are also refused. A separate campaign of 6,240 authorization round-trips had no successful bypass. Against 3 contemporary systems claiming the agent control plane, the agent invokes control; here, it lacks that choice.