AI with Authority, from Application to Silicon: A Solo Researcher Tapes Out a Verified RISC-V Chip in Five Weeks (arXiv 2608.21356)

Forum topic · 小凯 · 2026-08-25

Summary

This paper (arXiv:2608.21356) reports that generative AI inverts the sixty-year-old cost relationship of machine verification, making formal verification economical and essential for productivity. In five weeks, a single researcher using consumer AI subscriptions directed a fleet of AI agents to build, from application code, through a verified compiler and executive, down to a RISC-V processor taped out on a community silicon shuttle—with no proof passing through human review and no RTL written by a human. The methodology, called the Salt method, relies on a proof kernel that no hallucinated proof can pass: mathematical claims travel between agents as kernel-checked artifacts, with human attention reserved for specification, design, and adjudication. Verification proceeds chain-of-statement style, from the Lean 4 kernel to SAT-checked equivalence at the silicon boundary. The authors release complete documentation, including theorem sources, pre-registered token meters, human-time lower bounds, and an append-only error ledger (256 catches, 2026-07-07 to 2026-07-20) with zero erroneous proofs on record.

Paper Overview

Field: Machine Learning
Author: Jason Hickey
Posted: 2026-08-21
arXiv: 2608.21356

Key Points

For sixty years, machine verification has been a major cost overhead, affordable only for exceptional artifacts. This paper reports that generative AI inverts that relationship: at AI speed, verification is economical and essential to productivity—the incorruptible referee that lets one person safely direct autonomous machine work at scale.
Result: 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.
Method — the Salt method: Built on a proof kernel that no hallucinated proof can pass. Mathematical claims travel between agents as kernel-checked artifacts; human attention is reserved for statements, design, and adjudication.
Verification chain: Statement-by-statement, from the Lean 4 kernel down to SAT-checked equivalence at the silicon boundary.
Released artifacts: Complete documentation including theorem sources, pre-registered token meters, human-time lower-bound constraints, and an append-only error ledger for the mathematical campaign.

Error Ledger

Capture counter reached #256 during 2026-07-07 to 2026-07-20 (capture #79 was never assigned; later captures are unnumbered records).
Against this ledger: zero erroneous proofs reached the record.

Abstract (from the paper)

> 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 betwee...

*Collected automatically on 2026-08-25.*