7.1. The thing we are proving against🔗

You cannot prove a processor "correct" in a vacuum — correct with respect to what? The answer is the instruction set: the contract that says what each instruction is supposed to do. In this book that contract is not prose in a manual, it is the function step from the semantics chapter — a real Lean program that takes a machine state and an instruction and computes the next state. Because it is executable, there is no ambiguity to argue about: the specification is an interpreter, and "the tessera is correct" means "the tessera does what this interpreter says."

That already rules out a whole category of hardware bugs — the ones that come from a specification nobody pinned down. Here the specification is pinned down to the bit.

7.2. Layer one: the pipeline is faithful to the instruction set🔗

Real hardware does not execute one instruction at a time; it overlaps them in a pipeline, and the danger is that the overlap does something the specification never sanctioned — a branch that fails to discard the instructions behind it, a result that lands a cycle too early. The Assembly Line chapter proves this cannot happen: pstep_refines shows that every clock cycle of the pipeline is either a stutter (nothing observable changes) or a faithful step of step, and pipeline_correct lifts that to whole runs — the pipeline, executed for any number of cycles, produces exactly the state sequence the instruction set prescribes. The fast, messy machine and the tidy specification are proved to agree.

7.3. Layer two: the hardware comes from the same source🔗

A proof about a model is worth little if the hardware is a separate artifact that a human retyped. In this project it is not. The register- transfer description that becomes SystemVerilog is generated — by lake exe emit — from the same Lean definitions the proofs are about, and continuous integration refuses any change where the committed hardware differs from what the generator produces. There is no hand-transcription step in which a bug could hide. The instruction encoding is proved invertible (decode_encode: decoding any instruction's encoding returns it unchanged), so the bits on the wire mean exactly what the assembler intended.

7.4. Layer three: the hardware executes the instruction set🔗

This is the theorem the book spent the longest reaching, and the story of how is worth telling because it is a genuine lesson about proving things about hardware.

The natural approach — take the emitted hardware description, evaluate it symbolically, and show the result matches the specification — ran into a wall. The evaluator that runs the hardware uses a string-keyed store (signal names to values), which is perfect for executing concrete test programs but, at the scale of a hundred-signal core, defeats symbolic proof: the reasoning engine drowns in nested conditionals that never collapse. We established that limit thoroughly before accepting it.

The resolution was to write the tessera's cycle a second way — tessStep, a plain function over a record of fields rather than a string-keyed store. Over records, reading a signal is a field projection that simplifies instantly, and the proofs that were intractable became one line each. The capstone, tessStep_arch_governed, says that in every cycle the tessera's architectural state is either held unchanged or advanced by exactly step — the instruction set — and nothing else. The register file, the accumulator, the scratchpad, and the program counter can only ever move the way the instructions say. From there tess_correct_from_init follows by induction: run the tessera from reset for any number of cycles and it computes exactly an instruction-set execution of the program — losing cycles only to pipeline fill, waiting on the mesh, and the two-cycle multiplier, never doing anything the instruction set forbids. For all inputs, not just tested ones.

7.5. The seam, named honestly🔗

That leaves one connection stated concretely rather than symbolically: that the emitted hardware description and the structured model tessStep compute the same thing. Both are proved to agree with the instruction set — the model symbolically for all operand values (tess_correct), the emitted hardware concretely on every instruction class, re-checked on every build (the ASTCheck suite runs each opcode through the actual hardware evaluator and through the specification and confirms they match). They meet at the instruction set, the common reference. The one thing not bridged by a single ∀-quantified proof is exactly the string-keyed evaluation the previous section showed to be intractable at core scale — so we route around it through the specification, and we say so plainly rather than implying more than we have.

This is the shape of honest verification: not "everything is proved" as a slogan, but a precise map of what is proved symbolically, what is checked exhaustively-per-case, and where the single seam lies.

7.6. What it adds up to🔗

Read the layers back to back. The instruction set is an executable contract. The pipeline provably refines it. The hardware is generated from the same source, not transcribed, with the encoding proved invertible. The hardware executes the instruction set — the model for all inputs, the emitted description on every instruction class every build. And beneath all of it, this book itself is the source: it does not describe a verified processor, it is one, re-checked every time it is built.

That is what the cover line means. The datasheet is a theorem — and now you have seen the theorem.