Architecture

One cell, repeated — and nothing above it.

Honeycomb keeps the hardware surface small enough to reason about: one cell, one ISA, one mesh interface, and one way to move data. Everything that is usually a special hardware role — boot master, DMA controller, memory hierarchy, security monitor — is either a program on an ordinary cell or a cost in the mesh.

One repeated cell

The basic hardware element is the Honeycomb cell. It contains local memory, scalar/control state, a MAC datapath for the kernel path, and nearest-neighbour network ports. The same cell is used throughout the compute fabric; its only outward difference is its coordinate.

That uniformity is a verification choice. Each extra kind of core, tile, cache, memory tier, boot agent, or privileged controller would add another behavior to specify and another interface to prove. Honeycomb instead proves one cell and composes it uniformly. Distance still matters, but it is a cost in the mesh rather than a named hardware tier.

A cell has:

• local memory holding instructions, scalar data, resident weights, and streams;
• scalar/control instructions for ordinary control flow;
• a MAC datapath for the resident-weight kernel path;
• nearest-neighbour links for explicit movement;
• the same boot ROM as every other cell.

One ISA, two workloads

Honeycomb uses the same cell for two kinds of work.

The kernel path is static and dataflow-like: resident weights are read from local SRAM, operands move explicitly, and schedules can make exact timing claims. The control path is an ordinary small computer: it boots, loads programs, handles coordination, and runs data-dependent branches. Its timing claim is bounded worst case, not exact cycle equality.

Using one ISA avoids a separate conductor core. The price is a modest amount of scalar and branch logic in every cell; the benefit is a single semantic contract for both the fast path and the control path. The contract is exercised end to end: the same coordinate-selected cell that runs kernel MACs also runs an interpreter for compiled RISC-V in simulation, with no separate core type.

Memory as a cost-space

Honeycomb does not make software name a memory hierarchy. Every object is addressed through a flat namespace and differs by cost: local SRAM is cheap, a neighbour is a hop away, and an external memory node is slower and larger.

cost = < distance (hops), latency, access granularity, capacity class >

own cell memory   < 0,      1 cyc,   word,  small >
neighbour cell    < 1 hop,  few cyc, word,  small >
DRAM node         < far,    100s,    block, large >

Local SRAM is for bandwidth and deterministic access, not for storing every byte a system might need. A large DRAM pool is still necessary for cold data, model loading, datasets, and checkpoints. Honeycomb treats that DRAM as a region of the same cost-space: a memory node presents the mesh interface, even though the controller behind it is different silicon. Bulk memory is fronted by a small number of gateway tiles; every other tile reaches it by a capability-gated get/put over the mesh, so the compute fabric itself carries no memory port.

The practical first form is DRAM attached at the array edge. That leaves some cells farther from bulk memory than others, so schedules must account for the distance. A later package could put memory under the array and make that cost more uniform. The programming model is the same in both cases: movement is explicit and schedulable.

Placement resolves names

Programs name values and tensors, not region+tile+cell+bank addresses. Placement resolves each name to a physical (node, offset), and routing turns movement into explicit copies. Locality is exposed as cost information; software does not depend on a fixed physical coordinate.

This matters for reliability too. If a physical cell is bad, placement can disable it and remap names elsewhere. A uniform array makes every healthy location a possible spare.

Deterministic movement

There is no cache coherence protocol and no implicit remote load. Movement is expressed as operations such as copy, fill, launch, and barrier, with explicit completion. Routing is dimension-order over the 2-D mesh: the transport model proves a packet arrives at its destination in exactly its Manhattan distance in cycles, payload intact, touching no other cell, and the routing discipline carries a proved acyclic channel-dependency argument. The generated fabric adds flow control — a blocked packet waits under backpressure rather than being dropped, and contending packets are arbitrated so that none is lost.

Static-rate kernels can therefore be scheduled ahead of time; control code can still branch, but within a bounded machine model. The verification page states exactly which of these properties are theorems, which are proved at the RTL level, and which are carried by golden tests today.

Boot without a master

The array does not need a privileged tile to start. Every cell has the same boot ROM. On reset, cells run identical code, discover their own position, and organize distributed startup with no central sequencer: the cell that finds itself at the origin loads and launches its neighbours, and every other cell halts and becomes loadable. One tile can load a program into another’s instruction memory and start it — but only while the target is halted, and only with the right capability. Edge devices such as storage, console, and DRAM are attached to ordinary edge cells and driven by programs.

The boot image is the trusted computing base. The trust target is a measured boot path: replicated ROM verifies the first image before executing it, and later stages are checked against the same architecture contract used by the Lean model.

Capability isolation

Cooperation across the fabric is gated, not ambient. The boot image provisions every tile with a capability: a 64-bit token plus a mailbox window, and an injection budget. A delivered packet takes effect only if its token matches exactly, and a data write lands only inside the target’s mailbox — so a peer cannot reprogram a running tile, cannot restart it, and cannot reach its working set or its capability register. In the model these are theorems (acceptance is exact token equality; writes are mailbox-confined; private state is unwritable), and the capability decode logic in the generated RTL is proved to compute exactly the model’s decision. A per-tile injection quota bounds any single tile’s footprint on the shared fabric.

This is what makes mutually-distrusting workloads on one array a design point rather than an afterthought: isolation is part of the delivery path, anchored in the boot ROM, not a privileged software layer added later.

Self-hosting

Self-hosting is a trust goal, not a performance claim. The machine should be able to load, verify, and launch its own next stage — assembler to loader to scheduler — with every step governed by the same halted-gate and capability rules as any other remote effect. The fabric already scatters programs, launches them, and gathers results with no host involvement past bring-up; the near-term target is the deterministic fetch-after-write rule that lets generated instruction memory become fetchable, proved once and used everywhere.

Proof surface

The verification story is intentionally small:

• one proved cell — memory, MAC, control semantics, and execute-path refinement;
• one uniform composition — the mesh theorem over identical cells;
• one movement model — explicit packets with proved delivery properties;
• one isolation mechanism — capability decode on the delivery path;
• one boot contract — replicated ROM and measured startup.

The design is not simpler for style. It is simpler because each omitted special case is a proof obligation that does not have to exist.

What cannot be flattened

Some non-uniformity remains and is part of the model:

1. Distance — a far node costs more than a near one.
2. The edge — external devices attach somewhere.
3. DRAM controllers — bulk memory is different silicon behind a uniform interface.
4. Capacity — local SRAM gives bandwidth, while large storage still lives outside the cell.