AI with Authority, from Application to Silicon: One Researcher Tapes Out a Verified RISC-V Chip in Five Weeks

Forum topic · 小凯 · 2026-08-25

Summary

This paper (arXiv:2608.21356) by Jason Hickey reports that generative AI has inverted the traditional economics of machine verification. For sixty years, formal verification was a costly overhead affordable only for exceptional projects; at AI speed, the author argues, it becomes economical and essential—acting as an incorruptible referee enabling one person to direct autonomous machine work at scale. In five weeks, a single researcher using consumer AI subscriptions directed a small fleet of AI agents to build a complete stack 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 discipline, called the Salt method, rests on a proof kernel that hallucinated proofs cannot pass: mathematical claims move between agents as kernel-checked artifacts, while human attention is reserved for statements, design, and adjudication. Verification proceeds chain by chain, from a Lean 4 kernel to SAT-checked equivalence at the silicon boundary. The full record is released, including theorem sources, preregistered token metering, human-time lower bounds, and an append-only error ledger (capture count reaching #256, spanning 2026-07-07 to 2026-07-20), with zero erroneous proofs reaching the record.

Overview

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

Abstract (full translation)

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, design, and adjudication. Verification proceeds chain by chain, from the Lean 4 kernel to SAT-checked equivalence at the silicon boundary.

The authors release the complete record: theorem sources, preregistered token metering, human-time lower bounds, and an error ledger --- whose capture numbering reached #256 --- a monotonic counter on an append-only ledger for this mathematical campaign, maintained from 2026-07-07 to 2026-07-20 (number #79 was never assigned; subsequent captures are recorded unnumbered) --- against zero erroneous proofs reaching the record.

Key takeaways

Generative AI makes machine verification economical and central to productivity, rather than a luxury cost.
End-to-end result: from application code to a taped-out RISC-V processor in five weeks, with no human-reviewed proofs and no human-written RTL.
The Salt method: a hallucination-proof kernel-checked workflow where humans handle statements, design, and adjudication only.
Verification chain spans the Lean 4 kernel down to SAT-checked equivalence at the silicon boundary.
Full provenance released, including an append-only error capture ledger (#256 peak capture) with zero erroneous proofs reaching the record.