Honeycomb

Honeycomb

One memory-rich cell, repeated into a whole machine.

Honeycomb is a processor for inference that is limited by movement, not arithmetic. It is a flat two-dimensional array of one repeated cell, with commodity DRAM at the array edge and nothing above the cells — no host, no cache hierarchy, no privileged controller. The architecture contract, executable semantics, refinement proofs, and generated RTL are one Lean artifact checked by one build.

The cell

The entire machine is built from one element. A Honeycomb cell holds local SRAM for instructions, scalar data, resident weights, and streams; a scalar unit for ordinary control flow; a MAC datapath that reads resident weights out of SRAM; nearest-neighbour mesh links; and the same boot ROM as every other cell. There is no other kind of silicon in the fabric — no separate DMA engine, boot master, or conductor core. A cell’s role — kernel worker, boot root, memory gateway — is chosen by the program it runs, and its only outward difference is its coordinate. Architecture describes the cell and why uniformity is a verification choice.

The array

Cells tile into a 2-D mesh, and movement across it is explicit packets — no cache coherence, no implicit remote loads. The transport model proves a packet arrives in exactly its Manhattan distance in cycles, touching no other cell, and the routing discipline carries a proved deadlock-freedom argument. Bulk memory is commodity DRAM at the mesh edge, addressed as a far region of the same flat cost-space rather than as a named hierarchy: local SRAM is cheap, a neighbour is a hop away, DRAM is far and large. The array boots itself from the uniform ROM — a coordinate self-selects the root — and every remote effect a program can have is authorized by a capability check whose decode logic is proved against the model.

The arithmetic

Weights rest next to the datapath as block floating point: shared-exponent blocks of integer mantissas, executed on an integer MAC path. The kernel dot products the machine executes are proved equal to their exact mathematical values, with overflow excluded by proved fixed-width bounds — the numeric contract is a set of theorems about the stored format, not an empirical tolerance.

The construction

All of the above is defined once, in Lean: the ISA semantics, the cell implementations, the mesh transport, and the isolation mechanisms, related by machine-checked refinement theorems, with the SystemVerilog generated from those same definitions and rebuilt, golden-tested, and drift-checked in CI. There is no management engine and no vendor blob anywhere in the chain. Verification explains the construction method and states exactly where the proof boundary sits today.

What it is for

Interactive inference is limited by movement: batch-1 decode rereads every active weight each token, which is why a GPU delivers a small fraction of its peak in that regime. Honeycomb keeps weights resident, so decode speed is set by aggregate bandwidth at the weights’ resting place — the intended wins are latency-bound decode, long-context work, and deterministic serving, while compute-bound prefill is expected to be comparable at the same node, not better. There is no Honeycomb silicon yet, and every published number carries its evidence tag. Performance has the recorded physical anchor and the same-node GPU comparison; Landscape places the architecture among GPUs, wafer-scale, and the deterministic ASICs.

Where it stands

A generated, macro-backed cell has been taken through open-PDK placement and routing to a signoff-clean result — every memory clock-gated, the reset fully timed, energy measured on the routed netlist, and the netlist itself passing its golden suite and a lock-step ISA co-simulation at gate level. The fabric boots itself from the uniform ROM, distributes work under capability gating, and a tile-resident interpreter boots Linux to a login prompt on the FPGA rig — all on the same one repeated cell. Status tracks every claim, tagged proved, modeled, recorded, or target.