Honeycomb🔗

Honeycomb is a proof-first computer built from as little hierarchy as physics allows. Most of what we call a computer's structure is elective — distinct core types, memory tiers, a privileged boot master. Honeycomb keeps only the one non-uniformity physics forces, distance, and treats it as a cost, not a rank. What remains is a single cell, repeated across a mesh. The wager of this book is that minimal hierarchy and maximal provability are the same objective: every tier not built is a proof not owed.

The cell is a memory-rich element — standard-cell logic wrapped around local, macro-backed SRAM — so a resident-weight kernel runs against on-cell memory instead of reaching across a fabric or out to DRAM. One cell and one ISA run everything: the branch-free kernel path that must move at full rate, and the general control code that boots, loads, and hosts the toolchain. These are not two machines but one substance under two workloads, differing only in how each uses the cell and in what it claims about timing — exact for static kernel schedules, bounded for data-dependent control, never in silicon.

The book is the source of truth. The definitions below are executable, the theorems are checked when the repository builds, and the generated RTL is not a separate description of the design: it is rendered from a Lean model whose execute path is proved to refine the ISA step function. A single lake build checks the semantics, the kernel and block-float arithmetic, and that refinement together — a page that builds cannot lie about the machine it describes.

There is no Honeycomb silicon yet. The first RTL artifact is a single-cell simulator and synthesis target whose execute path is proved against the ISA and which has been carried through sky130 synthesis with its hot memories bound as SRAM macros. The mesh above the cell is modeled and proved here — faithful, on-time transport composed with a uniform, pointwise composition that inherits the single-cell refinement — but its RTL rendering, the self-hosting path, parser-level SystemVerilog refinement, and every measured-silicon claim are future work; the Status and Evidence chapter that follows is precise about what is proved, modeled, recorded, and merely intended.