Honeycomb
A provably-correct processor for machine learning.
Honeycomb is one small, memory-rich cell, verified in Lean and tiled into a mesh. The RTL that goes to silicon is generated from the same proof that specifies it, so the design and its correctness proof are a single artifact.
Why it exists
On a GPU, batch-1 decode — a model answering one user, one token at a time — runs at well under 1% of the chip’s compute peak. Almost all of the arithmetic sits idle, waiting on weights that live in distant memory. Honeycomb keeps each cell’s weights in local SRAM and reads them straight into the datapath, so the work is not stalled on a far-off bus.
The other problem is trust. You cannot check that an ordinary accelerator computes what its datasheet claims; the specification and the silicon are separate things that are only ever compared by testing. Honeycomb is built so they are not separate. Every cell is the same verified element, and the whole machine follows from one specification, so there are no special cases to audit and nothing the datasheet can quietly get wrong.
How it compares to a GPU
The comparison is same-node: the process gap is set aside so it is about architecture, not fabrication. The GPU figures are measured on an RTX 2000 Ada running GPT-2; the Honeycomb figures are the target envelope from the fabric models.
| Workload | GPU (measured) | Honeycomb (target) | Evidence |
|---|---|---|---|
| LLM prefill (compute-bound) | 76,206 tok/s (100.0% of peak) | about 0.9×, comparable; MAC utilization ~89–91% | modeled |
| Decode, batch-1 (latency-bound) | 430 tok/s (0.6% of peak) | about 200× faster; weights stay resident, no memory wall | measured / modeled |
| Decode, batch-32 (throughput) | 8,523 tok/s (11.2% of peak) | about 9× faster; batching recovers some GPU throughput | measured / modeled |
GPU: RTX 2000 Ada, GPT-2, same-node. Percentages are computed from the book's recorded constants (gpuPrefillTokS, gpuDecodeB1TokS, gpuDecodeB32TokS).
Honeycomb wins where deployment latency lives, on batch-1 decode and long context. It is comparable on compute-bound prefill and behind on raw floating-point throughput. It is not faster than a GPU everywhere, and does not claim to be. What no GPU offers is a correctness proof.
How it’s built
rtl/honeycomb_cell.sv is not written by hand. It is generated
from a value in a Lean DSL, and the execute path of that DSL is proved to
refine the instruction set. A single lake build checks the
semantics, the arithmetic, and that refinement together, then emits the
Verilog. Golden simulations and open-source sky130 place-and-route take it
from there. If a generated file drifts from its source, the build fails.
Where it stands
There is no Honeycomb silicon yet. The first cell has been through synthesis, placement, routing, and timing on sky130: it routes to completion with timing met at every corner, and binding its memories as SRAM macros cut the design from 40,994 flip-flops to 802. The status page has the full picture of what is proved, what is measured, and what is still only intended.