用生成式AI实现从代码到芯片的全自动验证，让一个人高效主导大规模自动化设计。
AI with Authority, from Application to Silicon
- 通过可验证的AI代理链，全程自动执行从应用代码到硅片流片的全流程。
- 五周内完成无手动编写RTL的芯片流片，256个错误被记录但零错误进入最终记录。
- 适合关注自动化硬件设计、可信AI系统与形式化验证的工程师和研究者。
六十年来，机器验证一直成本高昂，仅限于极少数关键项目。本文报告生成式AI反转了这一关系：在AI速度下，机器验证不仅经济可行，更是提升生产力的必要环节——它作为不可篡改的仲裁者，使单人能够安全地规模化指挥自主机器工作。在五周内，一名研究人员依托消费级AI订阅服务，从应用代码出发，经由可验证编译器与执行器，完成了基于RISC-V架构的芯片在社区硅片穿梭计划中的流片，全程无人工审查，且无人工编写寄存器传输级（RTL）代码。其工作方法——盐法（Salt method）——依赖一个无法被幻觉绕过的证明内核：数学命题在各智能体间以内核验证的成果传递，人类仅负责声明、设计与裁决。验证过程逐链陈述，从Lean 4内核延伸至硅边界处的SAT验证等价性。我们公开完整账目：定理溯源、预注册代币计量、底限约束的人工耗时，以及一个错误清单，其中第#256项错误被捕获，而计数器自2026年7月7日至2026年7月20日持续追加，编号#79未被使用，后续捕获均无编号，但所有错误均被拦截，最终未有错误进入正式记录。
原文摘要 · Abstract (English)
For sixty years, machine verification has been a major cost overhead, affordable only for exceptional artifacts. Here we report that generative AI inverts this relationship: at AI speed, machine verification is not only economical but essential to productivity --- it is the incorruptible referee that lets one person safely direct autonomous machine work at scale. In five weeks, one researcher on consumer AI subscriptions directed a small fleet of AI agents from application code, through a verified compiler and executive, to a RISC-V processor taped out on a community silicon shuttle; no proof passed through human review, and no RTL was written by a human. The working discipline --- the Salt method --- rests on a proof kernel no hallucinated proof can pass: mathematical claims travel between agents as kernel-checked artifacts, and human attention is reserved for statements, designs, and rulings. Verification is stated link by link, from the Lean 4 kernel to SAT-checked equivalence at the silicon boundary. We publish the complete accounting: theorem provenance, a pre-registered token meter, floor-bounded human time, and an error ledger whose catch numbering runs to #256 --- a monotone counter over the mathematics campaign's append-only flags ledger, maintained 2026-07-07 to 2026-07-20 (one number, #79, was never assigned; later catches are recorded un-numbered) --- against zero incorrect proofs reaching the record.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。