具备权威性的 AI，从应用到硅片

六十年来，机器验证一直是一项主要的成本负担，只有非同寻常的成果才负担得起。在这里，我们报告生成式 AI 颠倒了这种关系：在 AI 的速度下，机器验证不仅经济，而且对生产力至关重要——它是不可腐化的裁判，使一个人能够安全地大规模指挥自主机器工作。在五周内，一名研究人员使用面向消费者的 AI 订阅，指挥了一小队 AI agents，从应用代码，经由一个已验证的编译器和执行器，一直到在社区硅片 shuttle 上流片的 RISC-V 处理器；没有任何证明经过人工审查，也没有任何 RTL 由人类编写。这套工作规程——Salt method——建立在一个任何幻觉证明都无法通过的证明内核之上：数学主张以经内核检查的工件形式在 agents 之间传递，而人类注意力则保留给陈述、设计和裁决。验证逐环节陈述，从 Lean 4 内核到硅片边界处经 SAT 检查的等价性。我们公布完整账目：定理来源、预注册的 token 计量器、有下限约束的人类时间，以及错误台账，其捕获编号一直到 #256——这是数学攻关的只追加标记台账上的单调计数器，维护时间为 2026-07-07 至 2026-07-20（其中一个编号 #79 从未分配；后续捕获记录为未编号）——同时没有任何错误证明进入记录。