AI with Authority, from Application to Silicon

Jason Hickey

cs.SEAug 21, 2026

AI with Authority, from Application to Silicon

Authors: Jason Hickey

Organizations: Karyk

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

\vdash P\in S

, adversarial tests T(P), and the certificate

S^{\prime}

with

\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.

Component	Size (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 stack	11,001 Lean lines
Silicon flow: importer, equivalence, cell models	4,251 Lean lines
Certificates (systems side)	1,884 Lean lines
Agent-written RTL	22,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\times 225.76\,\mu$ m $6\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\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

Aug 28, 2026

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

Modern artificial-intelligence coding agents can be equipped with tools for checking their own work e.g. a linter, a boot probe, a shell, a screenshot tool. We call this set the agent's verification surface. This study asks whether increasing only that surface, with everything else held fixed, produces a matching growth in the quality of the software the agent ships. We built a minimal coding agent whose tool list is the single controlled variable and used it to implement 1,116 web applications across six models and eight tool configurations. A condition-blind human graded every application against a frozen rubric, and automatic probes stress-tested the API-observable behaviors. Verification's cheapest benefit arrives first, which is to make sure that the application comes up. Without any tools, about one build in seven fails to launch at all and a single boot probe removes nearly all of these failures at roughly 35 percent of a full shell's token cost, while the full shell multiplies the no-tools cost by 2.35. Screenshots help most where mistakes are visible (e.g. element placement, interaction), though even there the gain over a shell is modest and does not survive correction for multiple statistical comparisons. In cases where failures can only be measured rather than seen, such as keeping scrolling smooth over a 100,000-row list, screenshots add nothing. A verification tool improves the output artifact only where its reach covers the way the application actually fails.

Achint Mehta

Automated Software Testing AI Coding Agents LLM Agent Verification Code Generation Evaluation

Ask PDF

Aug 13, 2026

Vero: Can AI Agents Build Formally Verified Software Repositories?

AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. Verified code generation, in which an agent produces both an implementation and a machine-checked proof of its specification, offers a stronger path toward trustworthy AI-generated software. Existing benchmarks in this direction either focus on individual functions or only evaluate proof generation with provided implementations. It is still an open question whether agents can make coherent implementation and proof choices across real multi-module codebases. To bridge this gap, we introduce Vero, the first benchmark to evaluate joint implementation and proof synthesis at the repository level. Vero contains 43 multi-module instances sourced from real-world repositories spanning Python, Dafny, Verus, and Coq, and covering diverse domains from cryptographic protocols to distributed systems. Each instance consists of a multi-module Lean 4 repository with predetermined API interfaces, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes. To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification or incorrectness of reference code, which surfaces and corrects latent code and specification errors during curation. We evaluate frontier coding-agent configurations with Lean toolchain access. The strongest agent fully solves only 27 of 43 instances and closes no specifications on the hardest repositories. Vero provides a concrete testbed for measuring progress toward repository-scale verified software synthesis, where current agents still fall short. We release the benchmark, curation pipeline, and evaluation harness at https://github.com/sunblaze-ucb/vero.

Zhe Ye, Hantao Lou, Yuechun Sun +8

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

Code Generation Formal Verification AI Agent Benchmarks Repository-Level Code Generation Code Generation Benchmarks

Ask PDF

Jul 15, 2026

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

AI coding agents produce code faster than humans can review it. In our approach, the prover is the judge of whether the code is correct. Under a verifier-driven loop, AI agents wrote and verified bare-metal security software in Ada/SPARK spanning classical and post-quantum cryptography, TLS 1.3, IKEv2, X.509, and a Matrix client. GNATprove discharged 49,280 proof obligations, established functional correctness for selected primitives, and proved the absence of run-time errors for the rest, at roughly 20-40 times lower supervision cost than comparable hand verification. GNATprove alone was insufficient: some defects could not be detected and were resolved using known-answer tests, interoperability, or human review of specifications. Given weak checks, the agent tried to bypass them and reported success. We report where each layer caught faults and draw the central lesson: what an agent can be trusted to establish is bounded by the strength of its feedback.

Tobias Philipp

secunet Security Networks AG, Essen, Germany

AI Coding Agents Code Generation Software Security Formal Verification

Ask PDF