A1–A4 公理

四条公理描述的是机制本身必须满足的性质。把它们写成公理而不是需求，是因为它们必须是接口性质——只有接口性质才能让第二实现照契约重写，而不是照第一实现的代码抄。

公理	内容	可由形式对象判定为
A1	无越权执行——任何动作都在有声明的能力域内	space 非空且 hi ≥ lo
A2	可审计——每次能力使用都留痕	guard 站点 ≥ 0，且编译期强制落审计计数
A3	模型缺席仍运行——单元不得申请模型 / 推理能力空间	space ∉ {ai, model, llm, net_llm, infer}
A4	失败计数与降级——可撤销能力必须声明 revocable	revocable 为真

为什么由形式对象判定

四条断言的输入不是源码，而是编译器强制导出的形式对象（Potato）。一个独立校验器仅凭该对象就能判定合法性——不读源码、不读二进制。这样一来，A1–A4 就从“运行时可能会检查”变成了“离线就能判定”。

目前做到哪一步： 断言表已经由形式对象生成（cap_asserts.rs），但尚未被内核 include! ——A1–A4 的运行时断言要等内核侧接入。当前只保证“表由形式对象驱动且逐字节对账”，不宣称运行时已在执行这四条。

延伸到 AGI 的那一步： A1–A4 的形式化推广（模型不可被理解时，边界是否仍可被审计）属于 FUAI Pro 的方向，与主线共用同一套数学底座。目前它是一条研究线，不是已实现的东西。