034 · AI 写的证明通过了，信任消失了吗？
Blanc 直接验证已部署的 EVM 字节码，让 AI 参与写证明，由 Lean 内核检查。值得追问的是：不再信任证明生成者以后，哪些判断仍留在证明之外？
Specification
030 · 只有 0.48% 通过，是模型失败还是评测失效？
SecTB-RTL 的 1,860 次调用只有 9 次通过执行端语义校验，但生成约定遗漏了执行端的复位规则。作者因此保留失败记录，却不报告提示词效果：完整分母也救不了失配的测量工具。
029 · 规则能执行，是否就忠实表达了政策？
NOMOS 把书面政策编译为确定性工具调用门控。它能排除自阻塞、参数错绑等结构缺陷，却仍可能把具体授权弱化为‘用户要求过某种操作’。
004 · RTL 与断言来自同一份规格，形式化证明了什么？
一条从受控自然语言规格同时生成 RTL 与形式化断言的工作流，以及它尚未消除的共同误解与证据边界。