cs.SEAug 21, 2026

AI with Authority, from Application to Silicon

Authors: Jason Hickey

Organizations: Karyk

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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.

Figures & tables

Figure 1: Figure 1 | The Salt method, in brief. The creed and the twelve articles — six required invariants and six advisory articles of the reference configuration. Required states what the method is; Advisory states what this case study ran and measured. The figure is designed to stand alone.
Figure 2: Figure 2 | The configuration and its product. One human directs a five-seat agent fleet sharing a repository and an append-only message bus, with the kernel beneath as the incorruptible referee; every objective returns five artifacts — the implementation P, the specification S, the kernel-checked proof ⊢P∈S\vdash P\in S , adversarial tests T(P), and the certificate S′S^{\prime} with ⊢S⇒S′\vdash S\Rightarrow S^{\prime} kernel-checked. The return arrow is the method’s reading surface: the human reviews the certificate and interrogates; no proof passes through human review. ⊢\vdash marks what the Lean 4 kernel checks — once for the implementation’s correctness, once for the specification’s comprehensibility.
Figure 3: Figure 3 | The spine as a chain of custody. The four parts and the links between them, each link labeled by its checker (Lean kernel; SAT equivalence; synthesis miter). The processor’s sequential state is shown at its measured provenance in the 2026-08-10 submission (288 of 902 flip-flops kernel-emitted, 31.9%; RTL-side 352 of 966 — the disabled fourth MAC island was correctly removed by synthesis); the shipped revision’s GDS has not yet received its structural join, and no die-level ratio is stated for it. The accompanying table gives each component’s measured size — sizes to be drawn beside the components in the final figure. The arc above traces the 1990 switching-network theorem from its publication to its kernel proof and its place on the submitted design.
ComponentSize (measured; extractors in Methods)
Verified compiler (DSL →\to ISA)5,067 Lean lines / 13 files (figure retired by docs/methods-size-manifest.md in the systems repo — the manifest’s file list is normative; the row re-derives from it at one sha)
Verified executive + application stack11,001 Lean lines
Silicon flow: importer, equivalence, cell models4,251 Lean lines
Certificates (systems side)1,884 Lean lines
Agent-written RTL22,679 Verilog lines across 71 files (silicon’s measured split, saltworks 456f508 — denominator reproduced first at 316,911/119; flow-generated netlists 294,232 lines/48 files excluded, 92.8%)
Table 4
Figure 4: Figure 4 | The shipped die, logic visible — two colorings. The submitted design (Tiny Tapeout shuttle run 32284710003, shuttle-repository commit 7d2b275), drawn from the shuttle’s own final placement. 43,884 placed instances occupy a 1030.40×225.76 μ1030.40\times 225.76\,\mu m 6×26\times 2 tile at 56.27% design-instance utilization (LibreLane). 11,212 are logic and are drawn; the remaining 32,672 are fill, decap, tap and antenna cells and are not drawn, which is what the white space is; the 6×26\times 2 die area is outlined, so the placed logic is seen against the true die edge. Top, function. Color follows function, and shade follows the member within a family: the fabric (including the RISC-V core and control) — 6,933: 3,739 combinational, 2,014 multiplexer, 1,180 sequential; the three MAC islands (1,149, kernel-emitted by the Lean-verified emitter, not “kernel-verified”), each physically interleaved with its serializer (294), which is why per-function boxes would overlap and per-cell coloring is the faithful form; clock distribution (214); hold & fanout buffering (2,397 — 1,267 hold-fix delay cells and 874 max-fanout buffers on data paths, plus 256 slew, capacitance and wire-length repairs); drive-strengthening (214); and ties (11). Of the die’s 1,468 flip-flops, 288 lie inside the named MAC and serializer groups and 1,180 in the fabric. Bottom, provenance — who authored each cell: agent-written RTL 6,944 (61.9%); tool-inserted timing repair 2,611 (23.3%); kernel-emitted 1,443 (12.9%); and clock distribution inserted by clock-tree synthesis 214 (1.9%), which is authored by nobody — a category as distinct from agent-written as from kernel-emitted. 1,443 cells (12.9% of logic) carry a surviving hierarchical name; the rest are anonymous after flattening.
Figure 5: Figure 5 | The forge. Commits per day over the campaign’s 37 consecutive days — zero silent days — stacked by repository: salt (mathematics, blue) and saltworks (system, orange), the dividing line at the system forge’s opening (Aug 5); milestone theorems flagged at their landing days. Inset: the corpus against mathlib, measured with the identical extractor at the pinned revision (29.3%).
Figure 6: Figure 6 | The economics, measured. ( a ) The pre-registered metered window: 116 h 40 m of wall clock (nights included), the human’s engaged floor of 37 h 21 m — machine-authored keystrokes excluded by the published correlation instrument — and the window’s totals. ( b ) Share of commits landing inside fleet-silence windows over the full campaign, by repository; the longest silent stretch containing landings ran 20 h 56 m and carried 26 commits.

Explore similar work

CardsList

  1. The reach of a verification tool decides its value: A controlled study of verification surface, artifact quality, and cost in AI coding agents

    Aug 28, 2026Achint MehtaAutomated Software TestingAI Coding Agents

  2. Vero: Can AI Agents Build Formally Verified Software Repositories?

    Aug 13, 2026Zhe Ye, Hantao Lou, Yuechun Sun +8Code GenerationFormal Verification

    1UC Berkeley · University of Chicago · 3California Institute of Technology +3

  3. The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK

    Jul 15, 2026Tobias PhilippAI Coding AgentsCode Generation

    secunet Security Networks AG, Essen, Germany