Status
Every claim, tagged. Nothing uncaveated.
Honeycomb is not silicon yet. The current artifact is a proof-and-RTL repository: executable Lean semantics, checked theorems, generated SystemVerilog, golden simulations, analytical models, and recorded sky130 physical-design runs. This board is generated from the same build that checks the proofs.
At a glance
The strongest physical result is honeycomb_cell_mac: a generated, macro-backed cell with powered SRAM macros that routes with 0 DRC violations, passes KLayout signoff DRC and LVS, and meets timing at all nine STA corners at a 29 ns clock (structural waivers enumerated in the evidence record). Binding the hot memories as SRAM macros cut mapped flip-flops from 40,994 to 802 — the difference between a proof/simulation memory shape and a physically plausible cell.
The strongest proof results reach the generated RTL itself: the compute cell’s execute tree and combinational read/decode stage are proved — as rendered design values under an evaluation semantics — to compute exactly one ISA step from the encoded instruction word, store write ports included; and the emitted router, flit, capability gate, and flow-controlled stations are proved the same way to compute exactly the model’s routing, delivery timing and isolation, capability decisions, and no-loss handoff under backpressure and contention. The routed signoff netlist passes its full golden suite and a randomized lock-step ISA co-simulation at gate level.
On the software side, the machine boots an operating system: a tile-resident RV32IMA interpreter, written in the machine’s own ISA through a Lean assembler (label resolution proved correct, undefined labels and unfitting offsets rejected at build time), boots the mini-rv32ima Linux kernel to a Buildroot login prompt on the Alveo U50 FPGA rig — at the reference emulator’s speed, with kernel memory served over the capability-gated fabric from HBM. Each instruction is additionally a golden test on genuine compiled machine code; the interpreter itself is tested, not proved.
Evidence table
Generated from the book data: 74 of 76 tracked claims are closed; 40 proved, 1 modeled, 33 recorded, 2 target.
| Claim | Evidence | State |
|---|---|---|
| fixed-width processor semantics | proved | closed |
| branch-free kernel dot correctness | proved | closed |
| cycle-level kernel scheduler refinement | proved | closed |
| block-float scale identity (an exact algebraic theorem: defer the shared scale to the block boundary; exponent/width/rounding representation is milestone-5 scope, stated in the chapter) | proved | closed |
| the machine computes the exact dot product (R5): n ISA steps of a resident kmac loop equal krun n under the prefix-fit obligation — both hardware wraps absorbed by the abstraction, accumulator exact as an integer (kmac_loop_exact) | proved | closed |
| quantized kernel no-overflow bounds | proved | closed |
| load lattice and utilization design rules | modeled | closed |
| GPU comparison constants | recorded | closed |
| generated single-cell RTL from Lean DSL | recorded | closed |
| single-cycle execute-path cycle-model refinement (cellExecCycle refines the ISA step) | proved | closed |
| cell execute stage refined at the AST level (R3): the generated case_-opcode statement tree, evaluated under a width/sign-aware semantics with read-stage wires pinned to the model, commits exactly execDecoded's pc/acc/pointers/halt/registers for every opcode and ALU funct — the hand-mirrored exec tree is no longer trusted by eye; preparing it caught and fixed the stw and funct-decode divergences | proved | closed |
| cell read/decode stage refined at the AST level (R3 complete): the base cell's combinational stage — field decode proved against the encoding layer, SystemVerilog's sign-extending widening assignments, operand formation, SRAM read addressing, and the st/stw write ports — computes from the sequential state and the encoded 32-bit instruction word exactly the overlay the exec-stage theorem consumes (cellRead_refines_envOf); the residual boundary is the honeycomb_sram read-port contract, whose address inputs are proved (cellRead_sram_addresses) and whose write ports carry exactly execDecoded's st/stw effect | proved | closed |
| pipelined-product exec arms refined (R3 complete): with prod pinned to the model's product for the committing instruction, the mac/fpipe dispatch tree commits execDecoded exactly on mac/kmac (cellMacExecC_mac/kmac); the fpipe tree is proved equal to the mac tree and, beyond the multiply arms, the dispatch is proved to select the base tree's own arm ASTs | proved | closed |
| encoded instruction fetch to execute-path refinement | proved | closed |
| abstract cell lifecycle refinement | proved | closed |
| fully synchronous-read cell refinement | proved | closed |
| pipelined fetch cell control-hazard refinement | proved | closed |
| generated pipelined-fetch RTL cell | recorded | closed |
| operand pipeline data-hazard safe-overlap theorem | proved | closed |
| full pipeline: composed fetch+operand overlap commits the ISA trace, one instr/cycle (proved) | proved | closed |
| run-level trace composition (R4): syncRun/pRun/fpRun are simulation theorems, not prose — 3n clocks of the sync cell, and the pipelined cells' computed schedules (at most 2n clocks, one per hit + two per bubble), each equal n iterations of the cycle model and, while the machine keeps executing, exactly n ISA steps (stepN) | proved | closed |
| generated synchronous-read RTL cell | recorded | closed |
| first-cell physical memory index contract | proved | closed |
| sky130/OpenLane inferred-memory synthesis attempt | recorded | closed |
| honeycomb_sram macro-adapter RTL boundary | recorded | closed |
| sky130 macro-adapter synthesis area | recorded | closed |
| sky130 macro place-and-route timing attempt | recorded | closed |
| pipelined-multiplier MAC closes timing (routed) | recorded | closed |
| pipelined-multiplier cell honeycomb_cell_mac (generated, golden) | recorded | closed |
| first routed macro cell: clean powered route, zero DRC, all nine corners met | recorded | closed |
| streaming kmac datapath: one MAC/cycle, routed clean on nine corners, 59 pJ/MAC measured | recorded | closed |
| generated general pipeline cell honeycomb_cell_fpipe (sync macros, read-stall interlock, golden) | recorded | closed |
| mesh transport and uniform-composition model | proved | closed |
| generated router and single-flit RTL from Lean DSL, golden-tested | recorded | closed |
| generated 1x2 multi-cell mesh RTL, host-write delivered across fabric | recorded | closed |
| cell-to-network aperture: net-store encodes the transport inject | proved | closed |
| network send is a conservative ISA extension (no regression, proved) | proved | closed |
| net-cell cycle model refines step and emits the packet, proved | proved | closed |
| dimension-order routing is deadlock-free (acyclic channel dependency) | proved | closed |
| generated net-cell and program-injection mesh RTL, golden-tested | recorded | closed |
| generated multi-hop line RTL: per-cell routers, store-and-forward, golden-tested | recorded | closed |
| generated 2x2 grid RTL: dimension-order routing turns a corner, golden-tested | recorded | closed |
| generated flow-controlled grid RTL: two packets contend, arbitrated, none lost | recorded | closed |
| general N×M mesh generator, emitted 3x3 with bidirectional links, golden-tested | recorded | closed |
| program on the mesh drives the fabric: cell-net st routes to a remote cell, golden-tested | recorded | closed |
| network backpressure: a net-store stalls until accepted, no packet dropped, golden-tested | recorded | closed |
| uniform tile array RTL: identical cell+router tiles, role by program, golden-tested | recorded | closed |
| remote boot: one tile starts another over the fabric, golden-tested | recorded | closed |
| remote boot loader: a tile loads a program into another's instr memory then starts it, golden-tested | recorded | closed |
| self-governed load capability: remote instr-write/start gated on target halted | recorded | closed |
| cross-tile schedule: one tile scatters work to several and gathers results, golden-tested | recorded | closed |
| hostless boot ROM: uniform image, coordinate self-selects the root, array self-boots, golden-tested | recorded | closed |
| capability-gated delivery: token+mailbox decode authorizes remote effects (unforgeable by exact 64-bit token, data confined to the mailbox, private state unwritable by peers) — proved, RTL twin golden-tested | proved | closed |
| fabric availability: round-robin bounded-wait fairness (now deployed in every station's arbiters, see R2 claim below) and a per-tile token-bucket injection quota bound a malicious tile's footprint (no starvation) — proved | proved | closed |
| router RTL refines the routing model: the generated honeycomb_router AST, under a DSL evaluation semantics, computes exactly routeDir/neighbour/arrival — proved | proved | closed |
| flit RTL refines InFlight.advance: under a sequential always_ff semantics the generated honeycomb_flit register update steps position by hop, carrying dst/payload, staying valid — proved | proved | closed |
| flit delivery timing refined: iterating the flit clock tracks InFlight.advanceN (hops k) and reaches the destination at exactly cycle manhattan src dst — proved | proved | closed |
| mesh delivery isolation refined: the generated per-cell delivery strobe fires for exactly the destination cell and no other (RTL image of injected_packet_delivered's isolation) — proved | proved | closed |
| capability decode RTL refines capDecode — all five effects (R6): the generated honeycomb_capgate, under the DSL semantics, computes exactly capDecode's effect including the read-tagged get gate (token via BitVec.toNat, op/is_read/halted mapped, 9-bit mailbox = inMailbox) — proved | proved | closed |
| capability hygiene (R6): the threat model is stated (adversarial programs, trusted fabric, plaintext tokens, guess-resistance-not-crypto); the allocator is proved well-formed (alloc_WF: bounded, pairwise-disjoint regions with pairwise-distinct tokens for the first 2^64 mints); the response-leg authorization gap is recorded at honeycomb_readresp | proved | closed |
| get response leg authorized (milestone 9, model): the read request carries a return capability and the reply is an ordinary capability-checked put through it — both legs of a lowered get are authorized at their gates, the served value lands in exactly the requester's reply cell and nowhere else, and a forged response is inert; the RTL echo of the return capability remains milestone-9 work (honeycomb_readresp still responds by convention) | proved | closed |
| flow-controlled station no-loss (per-input-port buffers): an input port accepts iff its own buffer is free, a live non-departing packet is held unchanged (backpressure never drops it), a departing one frees its buffer, a free buffer latches its port's offer — proved on the generated honeycomb_fstation AST | proved | closed |
| deadlock freedom transfers to the fabric's own resources: each station buffer is one directed channel, every wait edge strictly raises the buffer rank, and no ring of waiting buffers can close (no_bufwait_cycle) — the R1 shared-buffer head-on deadlock is structurally excluded, witnessed by the hline3 golden test (old station wedges, per-port station delivers both) — proved / recorded | proved | closed |
| flow-controlled hop (two composed stations): a concurrent-composition semantics for one east link proves a full link buffer holds the upstream (backpressure) and an empty one forwards the packet in one clock — it leaves the upstream buffer and arrives unchanged downstream, packet count conserved — proved | proved | closed |
| concurrent join (three composed stations, the fgrid2 corner): two upstreams offering one downstream on different ports the same cycle are both accepted at once — both upstreams free, both packets land unchanged in distinct per-port buffers, none lost — proved | proved | closed |
| output serialisation (one station, one link): two buffers contending for the same outgoing link are serialised by the deployed pointer round-robin arbiter — the winner's packet rides the offer and departs on the grant, the loser is held in place unchanged, and the pointer steps past the winner — proved (station_serialises) | proved | closed |
| round-robin fairness deployed in the fabric (R2): every station's output and delivery arbiters are the pointer scan rrFirst, with bounded wait proved against adversarial per-grant requests (rr_ptr_served_within: served within 5 grants); on the generated chain the rotated pointer serves the previous loser even against a refilled rival (station_serves_loser), and the tb_rrfair golden drives a line-rate flooder that starves transit under fixed priority but not under the deployed arbiter — proved / recorded | proved | closed |
| signoff-clean routed tile: honeycomb_cell_mac tightened to 2.49 mm^2 (2.24x), zero-DRC route, KLayout DRC + netgen LVS clean, setup/hold at all nine corners | recorded | closed |
| signoff-tile power ladder refreshed (R9): the record netlist (all memories ce-gated, nine-corner close) measured with the same vectorless and activity methods — 7.36 mW vectorless nominal TT (6.67-7.99 across corners), kmac 4.02 mW / 117 pJ per cycle / 0.58 nJ per MAC activity-driven; the gate-all result carries to the signoff tile, its 8-of-9-corner caveat is resolved, and the SRAM share of a running cell stays ~15% | recorded | closed |
| reset fully timed (R9): the blanket rst_n false-path — written for an old floorplan's quarter-nanosecond recovery miss, and silently untiming the reset's functional fan-in to the SRAM write enables — is removed; recovery, removal, and the functional paths meet at every corner on the record run, so the only remaining SDC exception is the combinational debug taps | recorded | closed |
| gate-level golden (R8): the routed signoff netlist and the routed kmac pipe pass their full golden suites at gate level (scripts/gls-mac.sh, gls-kmac.sh); the first run caught a real RTL-vs-netlist divergence — the clock-gated data macro froze the debug read port the RTL modeled as always-live — fixed by a one-cycle gate stretch plus a pulse read recipe, both now part of the RTL contract and exercised by both suites | recorded | closed |
| perimeter injection non-interference (milestone 8, model): destination-disjoint DMA injectors commute (dmaRun_comm — each injector's effect at a tile is a function of that tile alone), untargeted tiles are untouched, and each injector's weight/program regions land exactly as if it ran alone (dmaMultiRun_isolated + landed corollaries) — the region-to-injector assignment contract is the disjointness hypothesis; RTL rendering and the two-injector golden remain | proved | closed |
| assembler correctness (R10): pass 1's label map proved correct (asmFind_resolves), pass 2's emission indexed (asmEmit_get_blz/liLbl), and end to end an assembled branch encodes exactly the word distance to its label (assemble_blz_resolves); undefined/duplicate labels and unfitting offsets are build errors (the undefined-label hazard fired in production first — an orphaned branch target assembled to 0 and wedged the Sv32 walk), and a fitting offset survives encode/decode exactly (encWord_blz_imm_exact) | proved | closed |
| randomized lock-step co-sim (R8): seeded random programs with forward-only control flow (total by construction), their per-retire architectural trace computed by the Lean ISA step function itself, checked against the base cell every cycle and the five-phase signoff cell at every retire — at RTL and on the routed netlist at gate level — plus the final register file; covers out-of-range functs, full-range immediates, and wrapped memory indexes in bulk | recorded | closed |
| parser-level SystemVerilog refinement | target | open |
| Honeycomb silicon | target | open |
Not yet claimed
Honeycomb does not claim: fabricated hardware; measured silicon performance or power; a full-chip mesh; parser-level SystemVerilog equivalence; whole-grid multi-packet liveness (the concurrency proofs are compositional — two and three stations at a time, with buffer-level deadlock-freedom proved); or ISA-correctness theorems for the RV32 interpreter (its Linux boot is a recorded FPGA result, not a theorem). Each of these is either tracked work on the roadmap or a declared non-goal on the verification page.