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 authors present the Unfireable Safety Kernel, a Rust implementation that serves as an execution-time AI alignment layer for escapable AI systems. This system aims to provide authorization mechanisms for controlling such AI systems and ensures fail-closed invariants through machine-checked proofs.

What the Document Says

  • AI agents are given access to tools, APIs, etc., making them active principals in those systems.
  • The control mechanism is placed inside the agent's own runtime: system prompts, output filters, and guardrail libraries.
  • Any control reachable by inputs that influence it is a concern for AI systems with sufficient reach into their own runtime (escapable AI systems).
  • The authors identify four properties for an authorization mechanism to meet for architectural control: 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.
  • The authors position this layer as execution-time AI alignment, complementing training-time alignment (RLHF, Constitutional AI) and inference-time alignment.
  • They present a Rust reference implementation called the Unfireable Safety Kernel that realizes all four properties.
  • The fail-closed invariant of the Unfireable Safety Kernel 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).
  • The authors evaluate the kernel governing a live, escapable AI system and find that all 704 attempts on the safety-critical core are refused, with no escape, across 1,000 self-modifications.
  • In addition, a separate campaign of 6,240 authorization round-trips had no successful bypass.

Key Concepts Mentioned

  • AI agents
  • escapable AI systems
  • authorization mechanisms
  • execution-time AI alignment
  • Unfireable Safety Kernel
  • Rust
  • SMT theorem
  • bounded-model-checking

Claims Made by the Document

  • The control mechanism is placed inside the agent's own runtime.
  • 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.
  • The authors identify four properties for an authorization mechanism to meet for architectural control.
  • The Unfireable Safety Kernel realizes all four properties.
  • The fail-closed invariant of the Unfireable Safety Kernel is machine-checked.

Evidence Used

  • The text mentions that AI agents are granted access to tools, APIs, etc., making them active principals in those systems.
  • It is stated that the control mechanism is placed inside the agent's own runtime.
  • The text discusses the properties an authorization mechanism must satisfy for architectural control.
  • The authors present a Rust reference implementation called the Unfireable Safety Kernel.
  • The text mentions that the fail-closed invariant of the Unfireable Safety Kernel is machine-checked.

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.