# Roadmap **Status:** living document. Last revised 2026-09-01. Stage status is updated as evidence arrives. Nothing advances a stage without a recorded result, including a recorded *failure*. --- ## Stage status board | Stage | Topic | Status | Gate | |---|---|---|---| | 0 | Problem definition, taxonomy, threat model, harness | **DONE** | docs + harness exist and are used by a real experiment | | 1 | Simple arithmetic — zkVM fixed-cost floor | **DONE (E001)** | CP-001 answered with measurements | | 2 | Dot products — marginal cost, 1K→1M | demoted (see below) | CP-002 | | 3 | Matrix multiplication — the first research question | **DONE (E003)** | CP-003 | | 4 | Tiny neural network | queued | CP-004 | | 5 | Tiny transformer | **DONE via E018** | CP-005 / CP-016 | | 6 | Specialised ZKML / ZIP reproduction | queued | CP-006 | | 7 | Batching + recursion | queued | CP-007 | | 8 | Probabilistic verification | **E009-pre DONE** (falsified H9b); main CP-008 not started | CP-008 | | 9 | TEE / hardware attestation | queued | CP-009 | | 10 | Hybrid architectures | queued | CP-010 | | 11 | Scale / realistic inference | blocked on 2–10 | — | | — | **013 Work vs output** (correctness ≠ expenditure) | **DONE (E013)** | CP-011 | | — | **014 Numeric contract** (specifying arithmetic) | **DONE (E014)** | CP-012 | | — | **015 Non-linearities** (whole layer under contract) | **DONE (E015)** | CP-013 | | — | **016 Verification bandwidth** | **DONE (E016)** | CP-014 | | — | **017 Accuracy cost of the contract** | **DONE (E017)** | CP-015 | | 5 | **018 Tiny transformer + generation under the contract** | **DONE (E018)** | CP-016 | | — | **019 Interactive proof (sumcheck) for matmul chains** | **DONE (E019)** | CP-017 | | — | **020 Polynomial model — the price of provability** | **DONE (E020, E020b)** | CP-018 | | 10 | **Architecture decision** | **DECIDED (E020b)** — keep the model, pay the bandwidth | CP-010 | | — | **024 Layer-audit protocol** (built, not derived) | **DONE (E024)** | CP-022 | **Deviation actually taken on day 1:** after E001 measured the general zkVM at `R_prove ≈ 7×10^4`, we skipped ahead to Stage 3 rather than running Stage 2, because the urgent question was no longer "how does zkVM cost scale" but "does *anything* achieve `R_verify < 1`". E003 answered yes. Stage 2 is consequently demoted from a decision input to a record-keeping exercise. **Deliberate deviation from the suggested order:** two items are pulled forward out of Stage 8/9 because they are cheap, they gate everything downstream, and the evidence for doing so came from analysing v1 (`mvp-analysis.md`): - **E009-pre — heterogeneous replication divergence. DONE 2026-09-01, and it changed the programme.** Honest CPU-vs-GPU divergence turned out to be within a factor of 3.7 of the divergence caused by a real precision cheat, so no threshold separates them. Float-domain probabilistic checking cannot police precision cheating in a heterogeneous network. It still catches gross cheating. This falsified a conclusion in E003 and promoted quantised-integer arithmetic from a curiosity to the leading candidate fix. - **Coordinator-side metering.** Deriving token counts instead of trusting them closes the largest *currently exploitable* fraud vector in v1 at essentially zero cost. It is not research, it is a finding; it belongs in the v1 backlog. --- ## Checkpoints Each checkpoint is a question with pass/fail criteria fixed *before* running. ### CP-001 — What does a general zkVM cost at the floor? **ANSWERED** - **Question:** what does it cost to prove the smallest meaningful statement (`y = 3x + 5`), and how does that cost change as work increases? - **Success criteria:** a valid, verifying proof; prove/verify/size measured; a native baseline on the same machine; the fixed-vs-marginal split identified. - **Result:** see `experiments/001-simple-arithmetic/analysis.md`. ### CP-002 — How does proving scale with a large dot product? - Sizes 10^3 → 10^6 elements, integer and fixed-point. - Fit `prove_time ≈ a + b·n`; report `a` (fixed) and `b` (marginal), and the cycles-per-element the zkVM actually charges for one multiply-accumulate. - **Pass:** slope is measurable and stable across ≥4 decades; cost per useful arithmetic operation is quoted. - **Also:** the same dot product proved with a *specialised* argument (sumcheck / inner-product) to get the first zkVM-vs-specialised gap number (tests H3). ### CP-003 — Can a large matmul be verified far more cheaply than recomputed? **ANSWERED** *(the first research question)* **Result: yes.** Float32, k=40: `R_verify` = 0.023 (43.7× cheaper than recomputing) — but the clean guarantee holds only in exact arithmetic, and E009-pre showed the floating-point version cannot police precision cheating in a heterogeneous network. **Over a prime field on quantised-integer operands: `R_verify` = 0.046, soundness 9.1 × 10^-13 exact, no tolerance, no tuning.** Exact arithmetic costs 2× and buys back the whole guarantee. See `analysis.md` and `analysis-field.md`. Original plan, retained for the record: - Freivalds with `k` random vectors vs recomputation vs zkVM proof, for `n = 256…8192`. - **Pass:** `R_verify < 0.1` at soundness error ≤ 2^-40, with the error stated as a number, and the floating-point tolerance question addressed explicitly (Freivalds is exact over a field; float matmul is not — this must be handled, not hand-waved). - **Fail is informative:** if float tolerance destroys the soundness guarantee, that is a major result and redirects Stage 3–5. ### CP-004 — Full tiny NN (Linear→ReLU→Linear). - Compare zkVM, specialised, and Freivalds-per-layer + ReLU handling. - **Pass:** cost decomposition by layer type; identify which layer class dominates. (ZIP's Table 7 predicts *linear layers* will dominate at 93%; we should confirm or refute this at our own scale.) ### CP-005 — Tiny transformer: does attention change the picture? - Introduces softmax, layernorm, and a data-dependent access pattern. - **Pass:** measured cost split linear vs non-linear; verdict on whether the non-linearities or the matmuls dominate at small scale. ### CP-006 — Reproduce a ZIP-class result, or explain why not. - Attempt the LeNet-5 configuration on our hardware. Our machine is a 10-core M5; theirs is a 48-core Xeon with 512 GB. Expect to be slower. The deliverable is a *relative* number and a validated understanding of the method, not a competitive benchmark. ### CP-007 — Does batching or recursion reduce cost per job? - Batch N independent jobs; also segment one model into layer groups. - **Pass:** cost per job/token/CU is *lower* batched than individually, with the crossover N reported. **Do not assume it helps.** ### CP-008 — Can randomised verification reach useful security at <1% of recomputation cost? - Random segment audit over a committed execution trace. - **Pass:** a table of (audit rate, detection probability, cost, required stake to make cheating -EV). Security here is an *economic* quantity; report it as one. ### CP-008-pre — How far do two honest backends diverge? **ANSWERED** - **Result:** tolerance must inflate 191–381× to accept an honest Metal GPU; at that width a bfloat16 cheat passes. Separation between honest heterogeneity and cheating is ~3.7× (versus ~2,800× within a CPU-class network). The cause is the *device*: identical library, identical dtype, CPU vs GPU stream diverge by 765–3,069×. See `experiments/009-probabilistic-verification/analysis.md`. ### CP-009 — What does hardware attestation actually attest? - On available hardware (Apple Silicon Secure Enclave locally; TEE-capable cloud instances if procured). Map the attestation statement precisely onto Claims O/A/B/C/D/E and enumerate the trust set. - **Pass:** an honest statement of what is attested, its cost, and its trust set. **Fail case is fine:** "the available hardware attests X and X is not enough" is a result. ### CP-010 — What is the cheapest sufficient architecture? **DECIDED** - E020b measured the polynomial route at scale: the attention gap grows from +6.8% at 2 layers to **+19.8% at 8**, with softmax improving on depth while squared attention regresses. Nobody trades 20% quality for bandwidth. - **Decision: NC-0.3 lookup-table contract + one-random-layer audit + a stake equal to the job's compute value.** Works on an unmodified transformer, +1.4% perplexity, 39% of re-execution at 32 layers. See `architecture.md` §6. ### CP-018 — What does a sumcheck-compatible transformer cost? **ANSWERED** - **Result: nothing for activations, +4.2% perplexity for attention.** Replacing GELU with x² is free (−0.5%, inside noise); replacing softmax with squared attention costs 4.2% and is the change that actually enables the sumcheck. - **Corrects E019:** SafetyNets' networks had no attention, so "adopt quadratic activations" is not sufficient for a transformer. Softmax stops a sumcheck exactly as a lookup table does. - Leaves two measured architectures — see `architecture.md` §6. Likely floor, not estimate: softmax's advantage widens with scale. ### CP-017 — Can an interactive proof remove the bandwidth cost? **ANSWERED** - **Result: yes for matmul chains, no for our architecture.** A sumcheck verifies a 2-layer 2048² chain with a **792-byte** transcript against a 16.8 MB intermediate — **21,183×**, improving with scale. But applied to the E015 transformer layer the saving is **zero**: all 49.1 MB of matmul output feeds lookup-table non-linearities the verifier checks by recomputation. - **The tension it exposes:** NC-9 makes non-linearities lookup tables *because* a gather has no arithmetic to diverge; a sumcheck passes only through low-degree arithmetic. Determinism and provability pull against each other. This also explains SafetyNets' quadratic-activation restriction, which was necessary rather than arbitrary. ### CP-016 — Does the contract survive a transformer doing generation? **ANSWERED** - **Result: yes.** 10 prompts x 300 generated tokens, NC-0.3 contract, CPU vs GPU: **10/10 bit-identical.** Honest *float* backends: **9/10** — one pair diverged at token 72, so a ~10% false-positive rate makes output-hash replication unusable for enforcement. Quality cost **+1.4% perplexity** over ordinary quantisation, versus ~0 on MNIST. - **Two corrections to our own claims:** E009-pre's decoding-divergence prediction was wrong in direction, and NC-3 bounded the accumulator when the binding constraint is the **operand mantissa** (2^11 on MLX/Metal, not 2^24). Contract updated to NC-0.3 with clause NC-3b. ### CP-015 — What does the numeric contract cost in accuracy? **ANSWERED** - **Result: nothing measurable at 8 bits.** The extra cost of full integer determinism, over and above ordinary quantisation, is +0.0001 accuracy across three seeds on MNIST — one test image in ten thousand, and it changes sign. Real at 4 bits (+0.0038). CPU and GPU produced bit-identical logits on all 10,000 test images at every bit width. **Closes the last blocking unknown on NC-0.2.** Caveat: MNIST is easy, and no transformer or generation task tested. ### CP-014 — What does verification cost in bandwidth? **ANSWERED** - **Result: it dominates.** Verifying one layer needs 49 MB of intermediates against a 0.02 MB answer — 3,010×. Break-even needs compute worth $164/hour (cloud egress) against ~$1/hour for a real GPU. Every configuration loses. **The earlier `R_verify` figures are compute ratios that assumed a co-located verifier.** - **Rescued by auditing one random layer instead of all of them**: bandwidth is flat while compute saved scales with depth, so at L≥32 on cheap egress verification costs 39% of re-executing. Soundness falls to 1/L, and a stake equal to the job's compute value makes cheating negative-EV at any depth. - **Promotes interactive proofs (GKR/SafetyNets)** from interesting to the known solution: polylogarithmic communication is exactly what this cost demands. ### CP-013 — Can a whole layer go under an exact contract? **ANSWERED** - **Result: yes.** A transformer-shaped layer — three matmuls, softmax, GELU, layernorm, requantisation — produced **bit-identical** output on numpy-CPU, MLX-CPU and MLX-GPU at every shape. Non-linearities specified as integer **lookup tables** make divergence structurally impossible. Governing cost relation: **`R_verify` ≈ the non-linear fraction of the layer** (linear half checked at 0.33% of its MACs, non-linear half recomputed at 1.0× with zero soundness error). NC-0.1's scope limit is lifted → NC-0.2. - **Prediction missed:** we predicted `R_verify` < 10% and measured 47–96%, of which most is implementation overhead. See the analysis for which half is real. ### CP-012 — What does a numeric contract cost, and what does it buy? **ANSWERED** - **Result:** the expected supply/security trade-off does not exist. On integer operands every honest backend — CPU BLAS, MLX-CPU, MLX-GPU — returns the **bit-exact** product, so an exact contract admits 5/5 honest backends while separating cheats without bound. E009-pre's 3.7× window was an artefact of real-valued operands, not of heterogeneous hardware. Deliverable: `docs/numeric-contract.md` (draft NC-0.1). Covers linear layers only; non-linearities are the open question. ### CP-011 — What can correctness verification not see? **ANSWERED** - **Result:** against exact verification, every answer-changing cheat is rejected; the only answer-preserving exploit is a cached correct result, which a coordinator-side hash lookup closes. Strassen — a genuinely faster algorithm — is accepted, correctly. Literature searched: forcing useful work in software is possible but only under unproven hardness conjectures, and the PoUW SoK finds the economics do not work. **Claim C is conditionally achievable in software; Claim D is not.** See `experiments/013-work-vs-output/analysis.md`. ### CP-010 — What is the cheapest sufficient architecture? - Combine the survivors. Produce a decision rule as a function of job value, workload type and verifier capability. - **Pass:** a defensible tiered design with per-tier `R` and per-tier claim set. --- ## First 30 days (from 2026-09-01) Adjusted from the suggested plan where evidence has already changed the picture. ### Week 1 (Sep 1–7) — foundations *(largely complete on day 1)* - [x] Analyse v1; map its verification onto the taxonomy. - [x] Taxonomy, threat model, thesis, terminology. - [x] Literature: ZIP read in full; bibliography seeded from its reference list. - [x] Install and validate SP1 (6.5.0); benchmark harness written and in use. - [x] **E001 run — the zkVM fixed-cost floor is now a measured number.** - [x] **E003 run — Freivalds measured at `R_verify = 0.023`; CP-003, the programme's stated first research question, is answered.** - [ ] Install RISC Zero as a second zkVM, so E001/E002 conclusions are not SP1-specific. - [x] **E009-pre run — honest cross-backend divergence measured; H9b falsified and E003's precision-cheating conclusion retracted.** - [ ] File the coordinator-side metering finding against the v1 repo. ### Week 2 (Sep 8–14) — the marginal cost of proof - E002 dot products, 10^3–10^6, both zkVMs. - Fit fixed + marginal cost; derive **cost per proved arithmetic operation** — the single number that lets us extrapolate to any model size. - First extrapolation: what would a 0.5B-parameter forward pass cost on this curve? (Expect an absurd number. Record it; it defines the gap.) ### Week 3 (Sep 15–21) — ~~matrix multiplication~~ → exact arithmetic and real inference E003 and E009-pre both landed in Week 1, so Week 3 inherits their consequences: - ~~Quantised-integer Freivalds~~ **DONE** — `R_verify` = 0.046 with an exact 9.1 × 10^-13 bound. What remains is the other half: the **accuracy cost of quantised inference**, which is the price of the recommendation and is currently UNKNOWN. - **Cross-backend divergence on real decoding** (v1's llama.cpp stack, Metal vs CPU, temperature 0). Gives v1 the replication threshold it has never had. - Cross-vendor confirmation (NVIDIA TF32) that "float32 that is not float32" is a property of accelerators, not of MLX. ### Week 4 (Sep 22–30) — the first architectural decision - E004 tiny NN. - Begin ZIP reproduction only if Week 2–3 data says specialised proofs are worth the effort. - **Decision point:** commit the next quarter to whichever of {specialised ZK, probabilistic audit, TEE} the measurements favour — and write down what would change our mind. Schedule is subordinate to evidence. If Week 2 shows the marginal cost of zkVM proving is hopeless for linear algebra, Week 3 becomes probabilistic verification and specialised arguments only, and general zkVMs are demoted to a baseline we no longer invest in.