Verification

Not verified after the fact. Constructed so the proofs come first.

Honeycomb’s differentiated asset is a construction method: the architecture contract, the executable semantics, the refinement proofs, and the RTL generator are one Lean codebase, checked together by a single lake build. Verifiability is not a feature bolted onto finished silicon — it is how the machine is built.

One artifact

A conventional flow keeps the specification, the simulator, the RTL, and the physical design as separate artifacts, reconciled by test suites and review. Honeycomb collapses them: the ISA is a Lean function, each cell implementation is a Lean model proved to refine that function, the SystemVerilog is rendered from Lean definitions, and the golden simulation programs are Lean values whose expected results are themselves checked in Lean. When a definition changes, everything downstream either re-proves and re-emits, or the build fails. CI rebuilds the proofs, re-emits the RTL, rejects drift against the checked-in files, and runs the golden simulations on every push.

There are no sorrys and no axioms in the book: every theorem is closed, and the load-bearing ones quantify over all instructions and states, not test vectors.

What is proved

The proof stack, from the inside out:

• The ISA and its encodings. A fixed-width executable semantics (64-bit scalars and addresses, explicit wrap behavior, a fused kernel MAC), a checked bit-field layout, and a full decode (encode e) = some e roundtrip, composed so that generated program words drive the proved execute path.
• The cell implementations. A ladder of increasingly hardware-shaped cell models — combinational, fully synchronous three-phase, pipelined-fetch, and fetch+operand overlapped — each proved to commit the same architectural state as one ISA step, including the load-use stability argument, the branch squash-and-refetch, and a data-hazard theorem showing the operand interlock stalls only on genuine dependencies.
• The kernel arithmetic. Exact integer dot-product correctness, the block-scaled MAC identity that licenses shared-exponent blocks, prefix-fit overflow bounds discharged automatically for quantized blocks, and a conservation law proving the pipelined MAC scheduler retires the identical accumulator at any read latency.
• The mesh. Dimension-order transport delivers a packet in exactly its Manhattan distance in cycles, payload preserved, to exactly the destination cell; the network aperture is a conservative extension of the ISA (ordinary execution is untouched); and the routing discipline carries an acyclic channel-dependency theorem — the classic argument that dimension-order routing cannot deadlock.
• The capability layer. Acceptance of a remote effect is exact 64-bit token equality under a stated threat model; data writes are confined to the mailbox window; a peer cannot reach private state; remote reads are token-gated in both directions, and a read’s reply is itself a capability-checked write through a return capability the request carries — a forged response is provably inert. The allocator is proved to maintain disjoint regions with distinct tokens; a round-robin arbiter has proved bounded wait and a token bucket bounds any tile’s injection footprint; and destination-disjoint DMA injectors provably cannot interfere.
• RTL-level refinement. The proofs reach the generated RTL itself, for the compute cell and the fabric alike. The cell’s emitted execute tree is proved to commit exactly one ISA step for every opcode and ALU funct; its combinational read/decode stage is proved to compute that theorem’s every input from nothing but the sequential state and the encoded 32-bit instruction word — field extraction proved against the encoding layer, SystemVerilog’s sign-extending widening rule modeled where a plain mask would silently zero-extend — and the store write ports are proved to carry exactly the ISA’s memory effect. The pipelined-product execute tree of the signoff cell is refined too. On the fabric side, the emitted router, flit, and capability-gate modules are proved to compute exactly the model’s routing decision, one-hop advance, delivery timing and isolation, and capability decision — all five effects, including the remote-read gate; composed flow-controlled stations are proved, two and three modules at a time, to hold packets under backpressure, hand them off exactly, and serialise contention without loss; every station buffer is a directed channel in a proved-acyclic wait relation, so the deadlock-freedom argument holds on the hardware’s own resources; and the deployed round-robin arbiters carry the proved bounded-wait theorem.

The evidence taxonomy

Every public claim carries one of four tags, and the status board tracks all of them:

• [proved] — a Lean theorem in the book.
• [modeled] — a checked analytical model using stated constants.
• [recorded] — a measured or externally observed result copied into the book.
• [target] — intended behavior, not completed evidence.

Numbers on this site are not hand-maintained prose. The Lean build emits them to a data file the site reads, and CI fails if the site’s numbers drift from the book’s. Physical-design figures are recorded from tool reports; the taxonomy exists precisely so a routed-estimate number can never masquerade as measured silicon.

The boundary, stated plainly

A verification story is only as good as its stated edges. These are Honeycomb’s, kept current as they move:

• The renderer is trusted. Theorems about generated RTL are about the design values the SystemVerilog is rendered from; the pretty-printer from those values to text is small and reviewable but unverified, and parser-level equivalence of the emitted text is a documented non-goal. Three independent checks triangulate the gap: the Lean-emitted golden programs run on the emitted text in an independent event-driven simulator; the routed netlist passes the same golden suite at gate level (a run that caught, and fixed, a real RTL-versus-silicon divergence in a clock-gated debug path); and seeded random programs are checked in lock-step against the proved ISA step function at every retire — at RTL and at gate level.
• What the cell’s AST theorems still lean on. The compute cell’s read/decode and execute stages are refined at the AST level; what remains outside those theorems is the few-line SRAM adapter contract (rdata = mem[raddr] — its address inputs are proved, the adapter is golden-tested) and the sequential reset/start wrapper, which is covered by the run-level trace theorems against the cycle model rather than by the AST semantics.
• Concurrency proofs are compositional, not global. Backpressure, exact handoff, arbitration no-loss, and buffer-level deadlock-freedom are proved for the composed stations and the fabric’s own buffer structure; a whole-grid, many-packet liveness theorem (interleavings plus fairness over a full mesh) remains open, tracked work. The multi-packet behavior of generated grids is exercised by golden tests today.
• Run-level theorems, closed. Every cell variant’s whole-run behavior is a machine-checked simulation theorem, not assembled prose: the synchronous cell’s 3n clocks, and the pipelined cells’ computed schedules (one clock per hit, two per bubble, at most 2n), each equal n iterations of the cycle model and, while live, exactly n ISA steps.
• The RISC-V layer is tested, not proved. The tile-resident RV32IMA interpreter boots Linux to a login prompt on the FPGA rig at the reference emulator’s speed, and every instruction is golden-tested on genuine compiled machine code. Its Lean assembler now carries real theorems — label resolution proved correct, undefined or duplicate labels and unfitting branch offsets rejected at build time, and a fitting offset proved to survive encode/decode exactly — but the interpreter itself carries no ISA-correctness theorem. It is an application of the machine, not part of the trusted base.
• Physical results are recorded, not proved. Routing, timing, DRC, and LVS come from open-source signoff tools and are published with their scope: which checks ran, which library corners exist, and which structural violations are waived. Power is activity-driven estimation on the routed netlist, not silicon measurement.

Each edge is either a permanent, declared non-goal (parser-level text equivalence) or has a tracked path in the roadmap. The discipline is the point: the boundary moves outward by proof, never by prose.

Why this matters

For most buyers, hardware assurance today means auditing a vendor’s process. Honeycomb offers something structurally different: the isolation mechanism, the boot chain, and the delivery path are theorems you can read, about definitions the RTL is generated from, in a repository you can rebuild. Determinism compounds the value — exact integer arithmetic and proved delivery timing make results reproducible bit-for-bit across runs and hardware revisions, which is a property no driver-stack can promise.

The book contains every definition and theorem referenced here, with the evidence tables generated from the same build.