AI agents produce Lean 4 / Mathlib kernel-checked proofs verifying a stack from application code through a compiler to RISC-V silicon.
Abstract
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.
Problem
Machine verification has historically been a costly overhead affordable only for exceptional artifacts, and generative AI produces fallible candidate proofs and designs whose trustworthiness is expensive to establish.
Approach
The Salt method has AI agents return, for each prompt, an implementation, a formal specification, a kernel-checked proof that the implementation meets the specification, adversarial tests, and simplified certificates restating the specification. Mathematical claims travel between agents as Lean 4 kernel-checked artifacts, so no hallucinated proof passes. 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.
Results
In five weeks one researcher directed AI agents to build a verified compiler, executive, and RISC-V processor taped out on a community silicon shuttle, with 2,087 commits in 37 days and zero incorrect proofs reaching the record despite an error ledger running to catch #256.
Figure 4: Figure 4 | The submitted geometry, logic visible. The shipped design (Tiny Tapeout shuttle run 32284710003, shuttle-repository commit 7d2b275), rendered as its placed logic — two colorings. Its measured sizes, each with its basis: 7,779 standard cells at synthesis (the committed synthesis stat — a synthesis count, not a placed-cell census); 14,636 placed standard cells among 43,884 insta
