PaperlayerView exact revision on arXiv

Source-linked AI summary

AI with Authority, from Application to Silicon

Jason Hickey

arXiv:2608.21356v1cs.SEcs.AIcs.ARcs.LO

TL;DR

Machine verification has traditionally been too costly for most development, while generative AI makes candidate generation fast without making trust automatic. The paper introduces and measures the Salt method, in which kernel-checked artifacts and structured review support one researcher directing AI agents across a verified stack to silicon. The case study reports a five-week consumer-subscription demonstration, link-by-link verification, and an error ledger reaching #256 alongside zero incorrect proofs entering the record.

  • Problem

    Formal verification has historically imposed substantial development and change costs, while generative AI has reduced candidate-generation costs without reducing the cost of trusting candidates.

  • Method

    Salt combines kernel-checked artifacts, preregistered requirements, structured opposition, and human review focused on statements, designs, and rulings across the development stack.

  • Results

    A single researcher used consumer AI subscriptions for five weeks to direct agents from application code through a verified compiler and executive to a community-shuttle silicon tapeout.

  • Takeaways & Limitations

    In this measured configuration, machine verification is presented as an economical precondition for AI-speed productivity rather than merely a production cost overhead.

  • Takeaways & Limitations

    The study is a single-expert case study, makes no claim of optimality or generalizability, and includes SAT-only hardware links because no general Verilog-to-Lean importer exists.

Abstract

from arXiv · show

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.

1. Introduction — a personal journey

The paper presents the Salt method as a case study in using formal verification to make highly autonomous AI development economically practical. In five weeks, one researcher directed AI agents from application software through a verified stack to a silicon tapeout, with complete provenance and error accounting.

  • The problem: Generative AI lowers the cost of producing candidate proofs and designs, but machine verification remains necessary for trusting them.The paper frames Salt as closing this gap between fast generation and reliable trust.
  • The demonstration: One researcher directed a fleet of AI agents from application code through a verified compiler and executive to a RISC-V processor taped out on a community shuttle in five weeks.The work began from empty repositories atop public mathlib and used consumer AI subscriptions.
  • The accounting: The case study documents every mathematical claim with kernel checks, replayable provenance trails, metered economics, and append-only error logs.The authors characterize the result as an existence proof with measurements attached, not as an optimal or general configuration.
  • The contribution: The paper contributes the Salt method, its full-stack demonstration, and measured accounting of economics, errors, and limits.Its central finding is that machine verification becomes economical and essential to productivity in the measured AI-speed regime.

Results

Salt treats verified development as a layered workflow in which machines check implementations and claims while humans review specifications, designs, and rulings. Its recurring artifacts and adversarial review process make statement-level trust part of the verification discipline.

  • Results: Trust requires checking both implementation and specification, because a proof is only as good as the statement it proves.The method therefore includes certificates that restate formal specifications in simplified vocabulary.
  • Results: Each agent returns an implementation, specification, kernel-checked proof, adversarial tests, and formal certificates for reader comprehension.The certificate layer supports human review of the statement while the kernel checks the proof implication.
  • Results: Human review begins with prose objectives, adversarial requirements review, a recorded interview, and preregistered acceptance criteria.The resulting prose requirements precede specification and implementation, preventing success criteria from being redefined after the work begins.
  • Results: Salt commits to machine-checked truth, structured opposition for what the kernel cannot check, and exclusive human attention to statements, designs, and rulings.Tasks are budgeted in advance, and an agent stops and reports failure when its budget is exhausted.
  • Results: The method defines six required invariants and six advisory articles, with the required tier tool-agnostic and the advisory tier specifying the measured configuration.The required invariants include checker-backed claims, append-only design records, unchanged statements during execution, and human control of irreversible acts.

THE SALT METHOD

The Salt method is summarized as a creed plus twelve articles: six required invariants define the method, while six advisory articles describe the reference configuration run and measured in this case study.

  • THE SALT METHOD: The method’s twelve articles divide into six required invariants and six advisory articles.Required states what the method is; Advisory states what this case study ran and measured.

3. The referee — the ground it stands on

The Salt method makes the Lean 4 kernel the sole arbiter of mathematical truth while using independent checks and recorded opposition across the workflow. Its hardware boundary is explicitly non-uniform, combining Lean kernel checks with SAT-based equivalence checks.

  • Mathematical referee: Every mathematical claim is re-checked by the Lean 4 kernel, so trust rests on the kernel and statement rather than the proof-producing model.Human review reduces to whether the claim checked and whether its statement expresses the intended one.
  • Hardware boundary: Hardware verification uses Lean for specification-to-artifact links and Yosys SAT-based equivalence for Verilog and synthesized-netlist correspondence.The paper states that no general Verilog-to-Lean importer exists in public artifacts as of 2026-08-11.
  • Operational controls: The five-seat configuration records design decisions and errors in an append-only ledger, with independent witnessing and adversarial refutation before execution.Measurement precedes assertion, and the extractor command travels with each reported number.
  • Error record: The mathematics campaign’s catch ledger runs to #256, while zero incorrect proofs reached the record and 73 registered headline theorems have commit-verified provenance.The numbering is a monotone counter; #79 was never assigned and later catches are un-numbered.
  • Five-artifact discipline: The workflow requires implementation, specification, kernel-checked proof, adversarial tests, and a kernel-checked certificate at every level.The human reviews the certificate and interrogates; no proof passes through human review.

5. The spine — the demonstration, from application to silicon tapeout

The demonstration carries a verified systems stack from application and compiler components through a multitasking executive to a taped-out silicon design. Its chain of custody names verification boundaries and distinguishes kernel-emitted hardware from agent-written RTL.

  • Demonstration scope: The stack was built in seven days of repository history within five weeks and includes a compiler, multitasking executive, and silicon design.The compiler targets a small instruction set and includes simulation proofs for its control constructs.
  • Silicon provenance: 902 flip-flops formed the measured sequential state, including 288 (31.9%) emitted from kernel-checked Lean artifacts and 614 from agent-written RTL.At RTL, the emission count was 352 of 966 (36.4%); the paper states both scopes because they answer different questions.
  • Tapeout: The design was submitted to Tiny Tapeout’s September 7, 2026 community shuttle and revised before shuttle close.The shipped design of record is the revised submission, identified by shuttle run 32284710003 and commit 7d2b275.
  • Theorem to hardware: The 1990 switching-network theorem is proved in the kernel, and its certified routing schedule drives the submitted switch.The full rotation-closure result is the theorem carried onto the design.
  • Chain of custody: The paper presents the modest hardware as evidence that one configuration can preserve chain of custody from theorem statement through verified compiler to physical design.Trust boundaries are named at each link rather than treated as a uniform verification process.

6. The forge — the mathematical foundations

The forge developed the Salt method through practical failures and produced a large, kernel-checked mathematical corpus. It formalized major results while leaving the twin prime conjecture unproved and distinguishing independent formalizations from claims of priority.

  • Method forged by practice: The method’s rules accumulated as case law from hallucinated results, plausible-but-wrong designs, and measurements quoted beyond their scope.The ledger records the incident behind every rule rather than presenting the method as designed in advance.
  • Corpus and pace: Over 320,000 lines of Lean 4 were produced in 37 days, measuring 29.3% of mathlib with the identical extractor.The paper also reports 658,103 lines by raw count, with both counting methods published.
  • Surveyed foundations: As of 2026-08-11, the surveyed corpus reported no public proof-assistant artifact for several major analytic-number-theory results, including Siegel–Walfisz and Bombieri–Vinogradov.The survey also notes that a live external Bombieri–Vinogradov project takes Siegel–Walfisz and the large sieve as named axioms.
  • Research provenance: Several results were formalized independently of near-simultaneous public artifacts and are reported as independent formalizations, not firsts.The paper cites Vaughan’s identity, the Maynard–Tao sieve, and the Montgomery–Vaughan Hilbert inequality in this context.
  • Boundary of the campaign: The twin prime conjecture remains unproved: within the corpus it is a definition, never a theorem.The campaign’s ambition therefore did not become a proof of the conjecture.
  • Kernel-checked mathematics: The corpus kernel-proved Maynard-class bounds, the least k with M_k > 2 is five, and a formal gap theorem for parity-invariant sieve certificates.It also formalized classical pillars while verifying the obstruction encountered by the campaign.

7. The economics

The campaign’s measured economics combine a pre-registered accounting window with autonomous execution and a documented retraction of an unstable cost ratio. Human attention shifted toward rulings while agents continued execution between them.

  • Scale and pace: 2,087 mathematics commits arrived over 37 consecutive days, while the systems repository received 1,379 commits over seven days.The mathematics repository averaged 56.4 commits per day and peaked at 178; the systems repository peaked at 343.
  • Measurement: 37 h 21 m of engaged human time was bounded within 116 h 40 m of wall-clock measurement, using an instrument that excluded machine-authored keystrokes.The estimate covers 45 engagement blocks and includes a stated four-minute uncertainty band.
  • The human’s role: Between periodic human rulings, the fleet worked autonomously at the execution layer without proofs passing through human review.The campaign recorded 20 council sittings, seven irreversible human acts, one design veto, and nine source verifications.
  • Accounting discipline: A verification-cost ratio was retracted after three runs differed by a factor of 52, including one run within the overhead range the claim had denied.The retraction was preserved in the ledger with an instruction never to quote a ratio of that class again.

8. What the referee exports

The kernel’s role extended beyond checking proofs: it anchored an error-correcting culture in which agents challenged scope claims, retracted errors, and converted incidents into written laws.

  • The error ledger records agents catching scope errors, including measured claims presented with the scope of laws.Other recorded classes included registers asserting world-state instead of measuring it and instruments used beyond validated configuration boundaries.

Discussion

The discussion argues that machine verification becomes a production precondition in a specific regime of fast, cheap, fallible generation, while emphasizing that the study’s evidence remains narrowly scoped.

  • When generation is fast, cheap, and fallible, the kernel is presented as a precondition for production rather than a tax on it.The paper links this regime to one person directing work without reviewing every proof, while reserving attention for statements and designs.
  • The demonstrated configuration is not claimed to be optimal, typical, or generalizable, and the subject is one formal-methods specialist.The paper characterizes its result as a single case study rather than an estimate of what other researchers, teams, or domains would achieve.
  • No physical chip result is reported: the design was submitted to a community shuttle, with estimated delivery in 2027 and no measured-silicon findings supporting the paper.The paper also states that the study contains no new headline mathematics and that its corpus formalizes known results.

Methods

The methods specify the reference configuration and its verification infrastructure for the case study, including pinned formal tools, audited axioms, and measured accounting.

  • The reference configuration used five agent seats, Lean 4 and mathlib pins, an axiom-audit protocol, and a disclosed verification chain for each link.The methods also specify tool versions, token-meter preregistration, human-time rules, survey procedures, and AI-use disclosure.

Data availability

The mathematics corpus, systems stack, error ledger, and submitted design files are publicly available or scheduled for release at publication. The work received no external funding.

  • Data availability: The mathematics corpus, systems stack, and error ledger have been public since 2026-08-16.Every theorem replays with one command.
  • Data availability: Remaining campaign registers, including the paper’s audit briefs, become public at publication.
  • Data availability: The submitted design’s files are on the shuttle’s public record.
  • Funding: The work received no external funding.
Loading 2608.21356v1…