这篇论文用Rust和形式化验证搞了个安全内核，1000次自修改加6240次授权测试都拦住了逃逸，比那些吹控制智能体的系统实在多了。
该论文提出Unfireable Safety Kernel，一种执行时AI对齐机制，满足四个属性：进程隔离、结构唯一路径预执行、请求和系统级故障关闭、外部可验证签名证据。Rust参考实现通过Z3定理证明和Kani模型检查（4/4 harnesses）机器验证了故障关闭不变性。在可逃逸AI系统上测试，面对逃逸攻击者，1000次自我修改中所有704次对安全核心的尝试被拒绝，无逃逸；6240次授权往返无成功绕过。相比3个声称控制智能体平面的当代系统，该内核使智能体失去控制选项。
The Unfireable Safety Kernel: Execution-Time AI Alignment for AI Agents and Other Escapable AI Systems
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.