AI with Authority, from Application to Silicon

TL;DR - This paper presents the Salt method, in which AI agents exchange machine-checked proofs while one researcher supervises development from application code through a verified compiler to a taped-out RISC-V processor. It argues that inexpensive formal verification can make large-scale autonomous engineering safer and more productive.

• Lean 4 proof-kernel checks prevent hallucinated proofs from being accepted as valid artifacts.
• Verification spans the toolchain link by link, ending with SAT-checked equivalence at the silicon boundary.
• The five-week project reportedly used consumer AI subscriptions, with no human-written RTL and no human review of proofs.
• Published auditing includes theorem provenance, token and human-time accounting, and an append-only error ledger recording 256 numbered catches, with zero incorrect proofs entering the final record.