Introduction

"If you wish to make an apple pie from scratch, you must first invent the universe." — Carl Sagan, Cosmos

The tower of trust

Between "my program ran correctly" and "electrons obey Maxwell's equations" stands a tower of trust: the instruction set means what its manual says; the processor implements the instruction set; the netlist computes what the RTL describes; the digital story the netlist tells is what the analog circuit actually settles to; the circuit is what the geometry realises; the geometry is what the fab printed; and the transistors do what the device models claim. Every program run in history has silently relied on every storey at once. Industrial practice verifies one or two of them and takes the rest on faith — reasonably, because the faith is grounded in decades of engineering discipline and billions of working chips, but the faith is unaudited: no one has ever written down, in one place, what exactly is being assumed at each storey and how the storeys compose.

This book is a scoping study for auditing all of it. The question it maps: what would it take to produce a machine-checked proof that one specific, physical, fabricable chip runs its programs correctly — starting from field equations over the silicon and ending at the instruction set? Not a chip designed to be verifiable, but a mainstream design produced by the ecosystem's own tools; not an idealised model of it, but the concrete artifacts the flow emits, distortions and datasheets and all.

It is not the proof. Carrying the proof out is a decade-scale project for a small group; the deliverable here is the map — for each layer of the tower, what the theorem is, how it would be proved, what it rests on, and what is genuinely unknown. The organising principle, adopted from the start: assume unbounded proof capacity, so that everything merely hard collapses to time. What survives that collapse — the claims no proof can reach, because they are empirical, or legislative, or genuinely probabilistic — is the result. The axiom register is the book's primary deliverable, and the six layer studies exist to justify its rows.

How correctness is established today

To see what is new here, it helps to know what the industry actually does — which is more, and less, than outsiders expect.

The overwhelming bulk of design verification is simulation: testbenches driving the RTL through billions of pseudorandom, coverage-steered cycles on server farms, with emulation hardware for the workloads simulation can't reach. It finds bugs with great efficiency and proves nothing. Formal methods entered the mainstream through a famous accident: the 1994 Pentium FDIV bug — missing entries in a division lookup table that shipped in silicon, cost Intel a $475M recall, and convinced the microprocessor industry that some properties are worth proving. The years after produced the field's industrial successes: floating-point units verified by theorem proving (AMD's division microcode in ACL2; Intel's FP algorithms in HOL Light), model checking — exhaustive state-space analysis of finite systems, the technique behind the 2007 Turing Award to Clarke, Emerson, and Sifakis — applied to protocols and control logic, and two formal-flavoured checks that became routine sign-off for every chip: equivalence checking, which proves the synthesised netlist matches the RTL, and static timing analysis, which covers all timing paths by construction. Below the netlist, no one proves anything: the geometric and physical storeys are governed by design-rule checking, layout-versus-schematic comparison, and manufacturing test — engineering disciplines with excellent track records and no theorems.

Academia has periodically tried to go end to end, and the history is instructive. The Viper microprocessor (UK Royal Signals and Radar Establishment, late 1980s) was fabricated and marketed for safety-critical use on the strength of a "proven correct" claim — and became the field's cautionary tale when Avra Cohn, who built the machine-checked proofs, published the sharpest analysis ever written of what such a claim can mean: the proofs related two formal models, neither of which was the physical chip; the verification was never completed down to the gates; and the storeys between the models and the silicon were exactly as unproved as anyone else's. Warren Hunt's FM8501 and FM9001 (1980s–90s, in the Boyer–Moore prover) verified real processor designs down to the netlist level — FM9001 was fabricated; the CLI verified stack (1989) composed a verified assembler, compiler, and processor into the first multi-storey artifact; Anthony Fox verified the ARM6 microarchitecture against the ARM ISA in HOL (the closest ancestor of this book's L3); the German Verisoft project (2003–07) verified the VAMP processor from ISA to gate level and built a verified software stack above it. More recently, the CakeML project's verified compiler runs on Silver, a processor verified in HOL4 down to its Verilog implementation and run on an FPGA — the vendor's Verilog-to-bitstream synthesis being the remaining trusted step — and Claire Wolf's riscv-formal brought bounded model checking to open-source RISC-V cores as an engineering practice. On the software side, CompCert and seL4 demonstrated that realistic compilers and OS kernels can be verified — and their experience with what a verification is conditional on shaped this book's ledger discipline.

Every one of these efforts stops at a storey boundary — the netlist, or an idealised gate-level model — and hands the rest to the fab's engineering. That is the gap this study is about: not any single storey, most of which have at least been attempted, but the composed statement about a physical object, with the physical storeys as theorems-with-hypotheses rather than background faith, and every surviving assumption in one auditable list. To our knowledge no one has stated that theorem before, let alone proved it.

The plan

The stance throughout is validation of an existing design, not design of a new one. The SoC at the centre was designed and is maintained by others — it is the mainstream of open hardware research, engineered to the ecosystem's best practices — and the job is to check that those practices delivered, not to re-engineer the artifact. This inverts the usual verified-hardware methodology — design for verifiability, then prove — and the inversion is the point: a theorem about a design anyone can regenerate, harden, and have fabricated says something a theorem about a bespoke academic core does not. Where a tool or an artifact cuts a corner, the finding is recorded (the register already holds several: two independent DRC engines return different verdicts on the same layout; a signoff step exhausts memory instead of reporting) and, if necessary, a minimal modification is priced. The proof architecture assumed is a hybrid one: a proof assistant hosting the statements and the glue, with untrusted industrial-strength tools — SAT solvers, synthesis tools, timing engines — admitted only through certificates their runs emit and small verified checkers replay. No tool is trusted; every tool is used.

One consequence of the stance is a rule about era: every artifact in the tower — RTL, netlist, constraints, layout, timing reports — is produced by one pinned flow, run by us, from sources we can modify. Nothing is inherited from a build that cannot be re-executed. The endgame of the study is tools that emit certificates as they run, and that requires tools that can be patched — which the layers below repeatedly cash in.

The target

The study is grounded in one artifact stack, chosen because it is the rare intersection of fully open and physically realisable. In 2020, Google and SkyWater Technology (a foundry in Bloomington, Minnesota, operating a former Cypress fab) released the SKY130 process design kit as open source — the first time the full design-side collateral of a commercial 130 nm process (design rules, device models, standard cells; the fabrication recipe itself stays in the foundry) was public. It remains the floor for open processes: no smaller node has an open PDK, so "modern" in this book means modern architecture and toolchain, never modern frequency. Merchant multi-project-wafer shuttles run against SKY130 continuously; the deliverable they accept is exactly the GDSII this book's flow emits, so the physical object at the bottom of the tower is a purchase order away rather than a hypothetical.

The design side sits on the stack that open hardware research has consolidated around. Chipyard (UC Berkeley) is the SoC framework: it composes a system — core, caches, interconnect, peripherals, debug — from parameterised generators written in Chisel, a Scala-embedded hardware language. Elaboration produces FIRRTL, an intermediate representation with a written specification, and CIRCT — the LLVM/MLIR hardware compiler — lowers it to SystemVerilog. The physical flow is Hammer, Chipyard's tool-abstraction layer, driving Yosys for synthesis and OpenROAD (a DARPA-funded academic effort) for place-and-route, with the venerable Magic layout editor — begun at Berkeley in the 1980s and still maintained — KLayout, and Netgen for the geometric and connectivity checks. On-chip memories come from SRAM22, an open SRAM generator for SKY130. Every input is pinned by commit and checksum; every artifact this book measures (RTL, netlist, GDS geometry, timing reports, constraint files) is regenerated by the flow in this repository.

The processor at the centre is Rocket — the original RISC-V implementation, begun at Berkeley alongside the ISA itself, the lineage core of the ecosystem (commercial RISC-V cores descend from it, and it has been fabricated dozens of times). The configuration is Chipyard's TinyRocketConfig, and the target follows the generated artifact exactly: a single 5-stage in-order RV32IMAC core with machine and user modes, physical memory protection, a 4 KiB instruction cache, a 16 KiB tightly-integrated data memory, a TileLink interconnect, a standard RISC-V debug module reached over JTAG, a CLINT and PLIC for interrupts, and a UART — with off-chip access carried by a serialised TileLink port at the pads. Simplicity is not the goal, realism is. The costs are recorded where they bite — machine-emitted SystemVerilog from a three-stage compiler pipeline, a pipeline and a cache in the refinement proof, generators whose semantics live in their implementation — and the study prices them rather than designing them away.

RISC-V, briefly

RISC-V is an open instruction-set architecture begun in 2010 at UC Berkeley (Krste Asanović, Yunsup Lee, Andrew Waterman, with David Patterson) — the fifth in the Berkeley RISC lineage that started with Patterson's RISC-I in 1981 and gave the reduced-instruction-set idea its name. Unlike x86 or ARM, the specification is freely implementable by anyone: stewardship passed to a foundation in 2015, now RISC-V International, and an ecosystem of open implementations grew around it — the ecosystem this book's processor comes from. Two features matter specifically for this project. The ISA is modular — a small base plus optional lettered extensions — so a small core can implement an honest subset rather than an apologetic fraction. And the standard did something this book leans on directly: RISC-V International adopted a machine-readable, executable formal specification (in Sail, a language purpose-built for ISA semantics) as its official golden model, which new extensions are required to extend as part of ratification. The spec this book verifies against is therefore not a private reconstruction from an English manual; it is the standard's own formal artifact, imported.

The six layers

The tower is cut into six layers. Each names an object — the abstraction at that altitude — and carries, as one of its subsections, the theorem that connects it to the layer above. Numbered by artifact altitude from physics up; bottom-up, since that is how the trust composes:

• L0 — physics. The device and field: from field equations and fitted transistor models to the electrical behaviour of the wires and transistors. Also the error model — what survives as genuine probability (particle strikes; almost nothing else). This is the one layer that carries ε; everything above it is deterministic.
• L1 — the electrical layer. The circuit as a space of transfer functions under a constraint system (this is where the old geometry and timing concerns merge). Two theorems live here: the drawn polygons, distorted within tolerances, still realise exactly the intended netlist with certified parasitics; and — the edge upward — timing closure, the combinatorial geometry/interference checks, and gain-based restoration together turn those transfer functions into a discrete synchronous machine (the bridge theorem everyone relies on and no one has stated). The layer trades ε for a constraint system.
• L2 — logic. The synchronous machine: flops plus combinational logic over a Boolean vector. Its edge upward is an equivalence, not an abstraction step — the hardened netlist and the source RTL denote the same machine, at gate and word granularity, by certificates rather than trust.
• L3 — RTL and microarchitecture. What the emitted SystemVerilog means: a formal semantics for the subset the design occupies (the same machine, word-level), and its edge upward — the theorem a computer architect would recognise, that the hardware refines the instruction set. The tower's irreducible proof.
• L4 — the ISA. The specification itself: the imported Sail standard, plus the parts that exist only as informal prose and must be formalised.
• L5 — the system. What the end-to-end claim is even about: the chip's observable behaviour at its pads, with the memory map, peripherals, and power in the specification where they belong.

Each layer names an object and, in one subsection, proves the theorem linking it upward; the layers compose along those seams into the top-level statement — the next chapter displays the whole chain. Two of those links are conditional on probabilistic events (a particle strike, an unresolved synchroniser), and those two conditions are exactly where the theorem's ε lives; everything else is deterministic. The book's chapters run top-down, L5 to L0, because the material gets progressively crunchier as you descend — and because reading the claim before its foundations mirrors how the trust is actually spent.

The overview that follows is the mathematical front door: the top-level statement, the objects at the seams, the dispatch of the proof into layers, and their prices. The appendices hold the ledgers — axioms, findings, the glossary, a reading list, and the bibliography. Everything else is the six layers.