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

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)

• Analyse v1; map its verification onto the taxonomy.
• Taxonomy, threat model, thesis, terminology.
• Literature: ZIP read in full; bibliography seeded from its reference list.
• Install and validate SP1 (6.5.0); benchmark harness written and in use.
• E001 run — the zkVM fixed-cost floor is now a measured number.
• 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.
• 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.