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