AI with Authority, from Application to Silicon
2026-08-21 • Software Engineering
Software EngineeringArtificial IntelligenceHardware ArchitectureLogic in Computer Science
AI summaryⓘ
The authors describe a new method where AI systems verify complex computer designs automatically, without human checking each proof. They used AI agents to build and verify a processor design in just five weeks, ensuring every step was mathematically checked by software. This approach makes machine verification faster, cheaper, and more reliable, allowing one person to manage the whole process safely. Their method centers on verified proofs passed between AI agents, with humans only reviewing high-level decisions and results. They also provide detailed records showing their system caught many potential errors and produced zero mistakes in the final proofs.
machine verificationgenerative AIRISC-V processorverified compilerproof kernelLean 4SAT-solvingRTL (Register Transfer Level)community silicon shuttletheorem provenance
Authors
Jason Hickey
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.