An expert used a five-seat AI fleet and formal verification to build and tape out a verified software-to-silicon stack in five weeks, with every theorem kernel-checked and provenance published. The case study shows that generative AI can invert verification’s historical cost barrier — making machine-checked assurance practicable at AI speed — but it is a single, specialist-driven demonstration rather than proof of broad productivity or economic effects.

Main Finding

At “AI speed” formal verification flips from an expensive exception to an economical, necessary referee: a single researcher, using consumer AI subscriptions and a five-seat agent fleet guided by the Salt method, produced a fully kernel-checked development chain from application to taped-out silicon in five weeks. Machine-checked artifacts (Lean 4 kernel + targeted SAT checks) provided a replayable chain-of-custody and an auditable error ledger; the experiment shows verification can enable safe, highly autonomous AI-directed engineering at much lower human cost than traditional verified projects.

Key Points

• The Salt method — discipline + tooling for high-autonomy AI development:
  • Every objective returns five artifacts: implementation, specification, machine-checked proof, adversarial tests, and a human-comprehensible certificate (a weaker, kernel-checked restatement).
  • Three core commitments: (1) truth only via machine checks, (2) structured opposition for what the kernel cannot check, (3) human attention limited to statements, designs, and rulings.
  • Six required invariants (R1–R6) govern correctness, recordkeeping, and human-only irreversible acts; six advisory articles (A1–A6) describe the reference configuration used in the case study.
• Fleet configuration and workflow:
  • Five long-running agent seats (coordinator, mathematics, compiler, silicon, evidence) share a repo and append-only message bus; one human orchestrates and performs only designated irreversible actions.
  • Agents are budgeted and must announce failures; every landing is independently witnessed and adversarially refuted prior to execution.
• Verification/referee stack:
  • Mathematical claims: Lean 4 kernel checking against mathlib (per-theorem axiom audits; only three standard axioms; no native_decide or custom axioms).
  • Hardware links: non-uniform chain with kernel-checked spec→emitted artifacts (link 1), SAT-based equivalence checks for Verilog↔netlist (links 2 and 4 via Yosys), and a synthesis miter (link 3).
  • Non-uniformity identified as a realistic boundary for small teams today (kernel covers what it can; SAT tools cover the rest).
• Demonstration and provenance:
  • One researcher, consumer AI subscriptions, five weeks (repositories started 2026-07-06).
  • Submitted silicon to Tiny Tapeout (initial submission 2026-08-10; shuttle run 32284710003; commit 7d2b275; shipped submission revised before Shuttle close).
  • System spine built: verified DSL→ISA compiler, verified executive (multitasking), and RISC-V processor with a certified routing schedule (1990 switching-network theorem proved in kernel drove the switch design).
• Measured accounting and error record:
  • Full accounting published: theorem provenance, pre-registered token meter, floor-bounded human time, append-only error ledger.
  • Mathematics campaign ledger (2026-07-07 to 2026-07-20) recorded a monotone catch counter up to #256 (with #79 unused); zero incorrect proofs reached the record (kernel-enforced).
• Size / extract metrics (as reported for the 2026-08-10 submission):
  • Verified compiler: 5,067 Lean lines (13 files).
  • Verified executive + application: 11,001 Lean lines.
  • Silicon flow (importer, equivalence, cell models): 4,251 Lean lines.
  • Systems certificates: 1,884 Lean lines.
  • Agent-written RTL: 22,679 Verilog lines across 71 files (netlists and flow-generated files mostly excluded from that denominator).
  • Processor sequential state (measured): 902 flip-flops on-die; 288 (31.9%) kernel-emitted at die level; RTL-side emission 352 of 966 flip-flops kernel-emitted (a fourth kernel-emitted MAC island was instantiated disabled and removed by synthesis).

Data & Methods

• Proof infrastructure:
  • Lean 4 kernel with mathlib pinning; per-theorem axiom audits limited to the standard three axioms; every mathematical claim rechecked by a compact independent kernel (LCF-style de Bruijn criterion).
  • No human ever reviewed proofs; human role limited to statement-level reading and rulings on certificates.
• Hardware verification chain and limits:
  • Link 1 (spec → emitted artifacts) checked in Lean.
  • Links 2 & 4 (Verilog ↔ synthesized netlist equivalence) checked via SAT equivalence (Yosys).
  • Link 3 is the synthesis miter; the campaign built importers/checkers scoped to flow-level netlist Verilog (no general Verilog→Lean importer exists publicly as of the dates reported).
  • Disagreements between independently-built checkers were recorded and reconciled at the byte level; these disagreements are in the ledger.
• Experimental controls and governance:
  • Pre-registered objectives and acceptance criteria; adversarial refutation passes; daily council for human rulings; append-only ledger records errors, retractions, and decision provenance.
  • Agent attempts were budgeted; failures are logged and escalate rather than being silently retried.
• Measurement provenance:
  • Measurements travel with extractor commands that produced them (instrumented reproducibility).
  • Campaign metadata: commit-extraction snapshot 2026-08-14; priority survey 2026-08-11.
• Limitations noted by authors:
  • Single-case study, run by a formal-methods specialist; not claimed to be typical or fully generalizable.
  • Non-uniform verification boundary for hardware remains (kernel cannot yet referee some links).
  • Some ledger catches beyond #256 unnumbered and unclassified; full-class breakdown only available for first 78 catches.

Implications for AI Economics

• Cost inversion and productivity:
  • Formal verification can become a cost-effective enabler rather than a prohibitive overhead when combined with generative AI agents and a small kernel trust base. This lowers the marginal human labor needed to produce high-assurance artifacts.
  • One skilled operator plus commodity AI subscriptions can substitute for multi-year expert teams on some verified-stack deliverables, shifting the economic model of high-assurance engineering.
• Shifts in factor composition:
  • Investment shifts from large specialist labor pools toward compute/subscription costs, kernel and toolchain infrastructure, and audit/verification services.
  • Human attention becomes the scarcest, highest-value input; systems that economize and price human review will be favored.
• Market and industry effects:
  • Lowers barriers to entry for producing verified software/hardware, enabling more actors (startups, individual researchers) to ship higher-assurance products.
  • Creates demand for standardized kernels, certified toolchains, and SAT-equivalence services; opens a market for independent witnessing/auditing agents and infrastructure.
  • Incentivizes detailed, machine-checkable provenance and metering as governance commodities (auditable ledgers, extractors, token meters).
• Governance, regulation, and risk:
  • Machine-checked proofs + transparent ledgers strengthen external auditability and liability allocation, which regulators and customers may prefer for safety-critical systems.
  • Non-uniform verification boundaries and dependence on specific kernels/tools create concentration risks and new single points of failure (trust in the kernel, in SAT tools, or in the chain-of-custody tooling).
  • Potential for misuse or overclaim if certificate layers or pre-registered objectives are weak; rigorous elicitation and adversarial practices are economically important.
• Labor and organizational impact:
  • Possible reduction in demand for distributed verification teams but higher demand for kernel/tooling specialists, verifier auditors, and people who can write precise requirement prose and perform statement-level review.
  • Organizations may reorganize around small orchestration teams supervising agent fleets rather than large engineering cohorts.
• Research and standardization priorities:
  • Economic value in maturing kernels, general Verilog→kernel imports, and uniform verified flows for hardware to reduce the current non-uniform verification boundary.
  • Standardized metrics, ledgers, and pre-registration instruments will be valuable public goods to lower transaction costs for trust and verification.

Caveat: this is a documented single-case demonstration by a formal-methods expert; the economic claims are empirical observations from that case with published measurements, not a proven general equilibrium result. Further replication and broader tests are necessary to determine typical costs, failure modes, and scalability.