Honeycomb🔗

Honeycomb is a proof-first processor architecture for memory-bound machine learning. It is built around one memory-rich cell, repeated across a mesh. Each cell keeps hot weights and streams in local SRAM, runs a small scalar/control ISA, and exposes data movement explicitly instead of hiding it behind caches or implicit remote loads.

The same cell serves two roles. Static kernel programs use resident data and a MAC datapath, where schedules can make exact timing claims. General control programs boot the array, load work, and coordinate execution, where the claim is bounded worst-case behavior. The point of using one cell and one ISA is to keep the semantic surface small: prove the cell once, then prove the uniform composition.

This book is the checked record of that surface. The definitions below are executable Lean programs, the theorems are checked when the repository builds, and several RTL artifacts are generated from Lean DSL values rather than written as separate hand-maintained descriptions. The central single-cell result is that the generated execute path refines the ISA step function.

There is no Honeycomb silicon yet. The book currently proves the processor semantics, instruction encoding, kernel arithmetic, scheduling invariants, single-cell refinement paths, and mesh transport/composition model. It also records golden simulations and sky130 physical-design runs for generated RTL, including a macro-backed cell that routes with powered SRAM macros. Parser-level SystemVerilog refinement, full-chip signoff, self-hosting, and measured Honeycomb hardware remain outside the closed proof boundary.