核心问题：当 AI 生成的证明通过内核检查，不再需要信任生成者之后，哪些信任仍然无法由这份证明替代？
论文卡片
- 原题： Verifying deployed bytecode against executable EVM semantics, with exact gas and no added axioms
- 作者： Seulkee Baek。
- 日期与版本： 2026-10-14 提交，arXiv v1；37 页；cs.PL / cs.LO。本文按预印本阅读，不视为已同行评审的结论。
- 定位： 字节码形式化验证系统 Blanc，以及 AI 辅助证明的案例研究；属于本专栏的“规格与可验证 Agent 工作流”方向，不是芯片设计实验。
- 阅读入口： arXiv · HTML 全文（v1） · PDF（v1） · alphaXiv
简短导读：检查证明，不等于替人选择命题
Blanc 面向已部署的 EVM 字节码：不可信程序提出结构化证书，Lean 内核检查它与字节码的对应关系，再相对于可执行语义 Jaune 证明性质。AI 在作者指导下参与写证明，而不是充当最终裁判。
证据与限制
论文报告八个验证对象。WETH9 的 gas 公式与筛选后的 3,748 笔交易回执吻合；另有 32 笔同类交易因起始余额难确定而排除。这是与真实执行费用的对照，不是全部定理前提的验证。
“无新增公理”指未超出 Lean 的三个标准公理，并非没有定理前提；WETH9 等旧合约的当前链上初始不变量尚未确立。语义忠实性与字节码来源也有证明外的信任边界。§4.2 还披露，一组旧定理对系统合约代码的前提并不符合真实代码，后来才修订。
AI 工作历时十五天，但依赖既有验证栈、人工指导，没有人工独立完成的对照组。它是案例证据，不是生产率基准。作者将主要困难归于命题含义；这属于经验判断，并非受控实验结论。
以上据原文 §2.4、§3.11、§5.3 与 §7；本导读未独立重跑证明。
重点阅读章节
- §2.1–2.4： 对照定理前提、结论与回执比较，留意三者回答的问题不同。
- §3.10–3.11： 看反例如何检验前提，以及内核检查的边界。
- §5.3、§7： 连读 AI 写证明的经历与局限，不只读“十五天”的数字。
思想启发：把信任拆开，才知道证明增加了什么
以下是导读者的思考，不是论文额外证明的结论。
我认为，理解这项工作的关键，是区分三个判断：推导是否有效、前提是否成立、命题是否值得证明。 一个判断更可靠，并不自动替另外两个背书。反过来，仍有证明外的判断，也不意味着内核检查没有价值：它把一部分原本依赖人的推理，变成了可明确审查的逻辑关系。
这也改变了“AI 会证明”的含义。若评价只看成功提交了多少证明，就可能混淆“找到了证明”与“选中了真正困难且重要的命题”。证明越容易批量产生，命题本身的范围、例外和解释反而越值得被单独讨论。
三个开放性思考问题
1. 一个前提写得完全透明，却尚未被证实成立，这份定理应获得多大信任？
参考思路
可以把对逻辑推导的信心，与对具体对象满足前提的信心分开。透明的条件至少让结论能够被准确限定；但“条件可检查”并不等于“条件已经检查”。难点在于：条件定理的知识价值，应主要由逻辑强度决定，还是由前提在现实中成立的可确认程度决定？两种评价未必给出相同排序。
2. 真实执行结果与公式反复吻合，能弥补形式化语义与现实之间多大的距离？
参考思路
经验吻合能排除部分模型错误，却未必触及从未进入样本的行为。另一方面，一份完全不接触实际执行的证明，也可能精确描述了错误的机器。值得讨论的不是测试与证明谁取代谁，而是它们各自留下的空白是否相互独立：如果样本筛选、模型和待检验结论共享盲点，一致性会不会显得比实际更强？
3. 若 AI 同时帮助写命题、写证明和解释证明，“解释听起来合理”还能提供多少独立证据？
参考思路
内核检查可以独立于生成过程，解释却仍可能沿用生成时的概念选择。换一个模型是否足够独立，取决于它是否只接受了同一套摘要与假设。反过来，要求人从最底层理解每一个定义，也可能让大规模证明难以被使用。这里尚未解决的张力是：我们希望证明降低对个人理解的依赖，却又需要理解来判断证明说的是不是所需之事。