ArXiv

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

Authors
Seth Dobrin, Łukasz Chmiel
Categories
cs.AI, cs.CR, cs.LG
arXiv
https://arxiv.org/abs/2606.26057v1
PDF
https://arxiv.org/pdf/2606.26057v1

Brief

The Unfireable Safety Kernel is a Rust reference implementation of an execution-time AI-alignment layer enforcing four architectural properties (process separation; pre-action enforcement on a structurally-only path; fail-closed at request and system levels; externalized signed evidence). It is machine-checked (Z3 SMT and Kani 4/4) and empirically refused all 704 safety-core modification attempts across 1,000 self-modifications. Full text not available; summary based on the abstract.

Why it matters

Unfireable Safety Kernel (Seth Dobrin, Łukasz Chmiel; 2026-06-24) is a Rust reference implementation of an execution-time AI-alignment layer that enforces four architectural properties: process separation; pre-action enforcement on a structurally-only path; fail-closed at request and system levels; and externalized signed evidence.

Key details

  • Formal verification and migration: the kernel's fail-closed invariant is machine-checked via a Z3 SMT theorem and exhaustive bounded-model-checking of the production decision function with Kani (4/4 harnesses). A Python→Rust migration was gated on byte-equivalence across 1,000/1,000 fixtures and 17/17 adversarial classes.
  • Empirical results on a deterministic, self-improving world-model agent: across 1,000 self-modifications all 704 attempts on the safety-critical core were refused with no escape; a further 300 attempts under the operator kill switch were also refused; 6,240 authorization round-trips showed no successful bypass.
Source evidence

Abstract

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.

Comment: Pre-print submitted for publication