AI with Authority, from Application to Silicon

The paper presents the Salt method, a workflow for directing autonomous AI engineering under machine-checked authority rather than trusting model output. Using five agent seats and consumer subscriptions running Claude-family models from Anthropic, one researcher spent five weeks building a verified stack from application code through a compiler, multitasking executive, and RISC-V processor design submitted to a community silicon shuttle, without human-written RTL or human review of proofs. Each task produces an implementation, specification, Lean 4 kernel-checked proof, adversarial tests, and a weaker certificate for human-readable review; mathematical claims are checked by Lean 4 against mathlib, while hardware correspondence and synthesis links use SAT-based equivalence checking in Yosys. The demonstration generated 2,087 mathematics commits in 37 days and recorded 0 incorrect proofs reaching the formal record, while an error ledger numbered catches through #256. At the silicon boundary, 288 of 902 sequential flip-flops in the measured submission were emitted from kernel-checked Lean artifacts, or 31.9 percent; the design was submitted, not yet physically fabricated. A preregistered 4.86-day meter captured 28.07M output tokens across 36,844 deduplicated requests and 56,951 inserted Lean lines. The central result is economic and organizational: when generative models produce artifacts rapidly but unreliably, formal verification becomes the enabling control layer, reserving human attention for requirements, designs, and irreversible rulings rather than routine proof inspection.