Reading list — getting up to speed

Introductory and canonical textbooks for the fields this project spans. The Bibliography cites specific results with verified identifiers; this list is pedagogy. Entries link to a registered DOI, the publisher's page, or the book's own site where one could be verified; the unlinked remainder are equally canonical and easily found. Where a work is also cited as a reference, it links to its Bibliography entry. Each entry says what it is for here, tagged by layer.

The project's centre of gravity for a reader arriving from formal methods is the hardware and the physics; for a reader arriving from hardware, it is the opposite. The first four sections are the important ones.

Computer architecture (L3–L5)

• Harris & Harris, Digital Design and Computer Architecture (RISC-V edition) — the single best on-ramp: gates → HDL → a working microarchitecture, in the project's own ISA. Read this and L3/05 becomes familiar territory.
• Patterson & Hennessy, Computer Organization and Design (RISC-V edition) — the standard first course, ISA-centric; the background for L4.
• Hennessy & Patterson, Computer Architecture: A Quantitative Approach — the graduate text; caches, pipelines, speculation, OOO. Read it to understand what L3/05's presence/absence table is pricing — each row of that table is a chapter of this book.

Electrical engineering (L0, L1)

• Agarwal & Lang, Foundations of Analog and Digital Electronic Circuits — uniquely apt here: it states the lumped-matter discipline as explicit assumptions before using it, which makes it the informal ancestor of L0/08's composition theorem. The rare intro text that admits where circuit theory comes from; the MIT course built on it is on OCW.
• Horowitz & Hill, The Art of Electronics — the practical canon; what real circuits do in the space between the theorems. The supervisor/BOR/decoupling material of L5/04 is bench knowledge from here.
• Sedra & Smith, Microelectronic Circuits — the standard devices-to-amplifiers course; the MOSFET-as-circuit-element background for L0/02.

Classical electromagnetism (L0/00–01, L1)

• Griffiths, Introduction to Electrodynamics — the undergraduate canon; everything L1's electrostatics needs, readably.
• Purcell & Morin, Electricity and Magnetism — the relativity-first treatment; the best answer to why magnetism is inevitable, and the right intuition for L0/01's EQS/MQS split.
• Jackson, Classical Electrodynamics — the graduate reference; boundary-value problems at the strength L0/09's enclosures actually require.
• Haus & Melcher, Electromagnetic Fields and Energy — the careful quasistatics treatment L0/01 leans on directly.

Quantum theory and solid state (L0/02, L0/05)

For this project the solid-state route is the load-bearing one — the QFT that matters for devices is many-body condensed-matter theory, not particle physics.

• Griffiths, Introduction to Quantum Mechanics — the standard first course.
• Ashcroft & Mermin, Solid State Physics — the canon: band structure, effective mass, semiclassical transport — the physical content behind E1, and most of what L0/05's tower actually rests on.
• Kittel, Introduction to Solid State Physics — the lighter alternative.
• Zee, Quantum Field Theory in a Nutshell — the friendliest QFT entry point.
• Peskin & Schroeder, An Introduction to Quantum Field Theory (or Schwartz, Quantum Field Theory and the Standard Model) — the standard course, either one.
• Altland & Simons, Condensed Matter Field Theory — field theory pointed at solids; the QFT that is actually adjacent to device physics.

Semiconductor devices (L0/02)

• Pierret, Semiconductor Device Fundamentals — the introductory device course.
• Taur & Ning, Fundamentals of Modern VLSI Devices — the modern MOSFET in depth; what BSIM is a fit of.
• Sze & Ng, Physics of Semiconductor Devices — the reference; avalanche and breakdown for L0/04.

VLSI and the physical flow (L1–L2)

• Weste & Harris, CMOS VLSI Design — the whole industrial flow in one book: layout, DRC, timing, clocking, the cell library. The layers' industrial counterpart, and the fastest way to see what L1–L2 are formalising.
• Rabaey, Chandrakasan & Nikolić, Digital Integrated Circuits — devices → gates → wires; its interconnect and delay chapters are L1's background.
• Bhasker & Chadha, Static Timing Analysis for Nanometer Designs — the industrial practice that L1/08 makes sound.

Mathematics of the lower layers (L0/00, L0/09)

• Evans, Partial Differential Equations — the standard graduate text; weak solutions and Lax–Milgram as L0/00 uses them.
• Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations — the toolkit behind row 3 and L0/09's variational bounds.
• Tucker, Validated Numerics — a short introduction to rigorous computation; L0/07's method in miniature.
• Moore, Kearfott & Cloud, Introduction to Interval Analysis — the interval-arithmetic foundation under every enclosure in the book.
• MacKay, Information Theory, Inference, and Learning Algorithms — for L0/03's coding half; freely available and a pleasure.

Formal methods (for the hardware reader)

• Nipkow & Klein, Concrete Semantics — operational semantics and machine-checked proof, hands-on; the mindset of L3–L3.
• Kroening & Strichman, Decision Procedures — SAT, SMT, bitvectors; L2's engine room.
• Biere, Heule, van Maaren & Walsh (eds.), Handbook of Satisfiability — the SAT canon in depth; the CDCL and proof-logging (DRAT/LRAT) chapters are the trust story behind every certificate in L1–L2.
• Avigad, de Moura, Kong & Ullrich, Theorem Proving in Lean 4 — an interactive-theorem-prover on-ramp, free online; the working style that every "formalise X" in this book assumes, whatever system the project ultimately inhabits.
• Pierce et al., Software Foundations — machine-checked program verification from zero (Coq, free online); volumes 1–2 are the discipline's boot camp, and CompCert is the flagship artifact showing where it leads — the verified-vs-validated-pass calculus L2/04 borrows comes from there.
• Clarke, Grumberg, Kroening, Peled & Veith, Model Checking — the standard text for the technique this project explicitly cannot use at scale (2^5774 states — L2/02) but borrows ideas from everywhere (IC3, invariants as certificates).
• Melham, Higher Order Logic and Hardware Verification — the historical centre of transistor-level formal verification; L0/06's ancestor.