Every measurement, including the ones that failed
Each experiment records its hypothesis before the run. Failed experiments are written up rather than dropped — they are the cheap ones — and three of the results here broke a conclusion the programme had already written down.
The chain, in discovery order
Genuinely a sequence: each result changed what the next experiment had to be, and several of them broke a conclusion that had already been written down. The full index follows underneath, grouped by status.
What does a general-purpose zero-knowledge proof actually cost?
Proving y = 3x + 5 on SP1 took 11.19 s against a native 0.69 ns. Proving ten thousand of them cost the same — the charge is for the existence of a proof, not the work inside it. The asymptote settles near 7 × 10⁴×, and that is a floor: register-resident u64 arithmetic is the friendliest workload a RISC-V zkVM will ever see. Not a tuning problem.
Can a large matrix product be checked more cheaply than redoing it?
Yes, by a 1977 result. Freivalds verified an 8192² product in 2.3% of recomputing it, soundness ≤ 2⁻⁴⁰, zero cost to the provider. Nine orders of magnitude better than E001 on the same claim — and the difference is not implementation quality. A zkVM pays for every load and branch in an execution trace; Freivalds exploits the algebraic structure of the statement.
How far do two honest backends diverge?
Far enough to ruin it. An honest CPU and an honest Metal GPU differed by 7.70 × 10⁻⁴; a genuine precision cheat by 2.84 × 10⁻³. The cause is the device — identical library, identical dtype, one line of difference.
falsified E003's security analysisIf the answer is right, did they do the work?
Seven cheating strategies against the strongest checker we had. Every strategy that changes the answer is rejected — but two low-work strategies pass, and should: a cached correct answer, and Strassen's algorithm at 67% of the arithmetic. No checker can object, because the answer is right. A shortcut is only an attack if you are paying for effort rather than output. The cache case is a pricing problem, closed by deduplicating on the input commitment.
What does an exact integer contract cost in supply?
Nothing. Every honest backend tested returns the bit-exact product, while cheats separate without bound. A whole transformer layer — softmax, GELU, layernorm, requantisation — came out bit-identical on CPU and GPU. Determinism is free at 8 bits, still free at 6, and costs real accuracy at 4.
reversed the expected supply/security trade-offWhat does verification cost in bandwidth?
Enough to dominate everything: 49.1 MB of intermediates against a 0.02 MB answer, and a break-even compute price of $164/hour against a real GPU-hour of about $1. We also rediscovered a 2017 result by construction here, because we had not searched the literature first. It is recorded in the experiment rather than quietly fixed.
killed verifying every layerDoes the contract survive a transformer that is actually generating text?
Only once we found the real bound. MLX's Metal matmul is exact on integer operands to 2¹¹ and inexact from 2¹², regardless of accumulator magnitude — so NC-3's 2²⁴ accumulator bound was 13 bits looser than the binding one. Attention probabilities carried at 2¹⁵ were the first operand to exceed it, and CPU and GPU generations diverged at token 102. With NC-3b in place: 10/10 runs bit-identical over 300 tokens each.
broke NC-3 · added NC-3bCan an interactive proof remove the bandwidth cost?
Sumcheck replaces a 16.8 MB intermediate with a 792-byte transcript — 21,183× — and the prover pays only 10.4% at n = 4096, of which the protocol itself is 0.5%. On a transformer layer it saves nothing, because every matmul output feeds a lookup-table non-linearity the verifier must recompute anyway. The tension is structural: the property that buys determinism blocks the proof. Making the model sumcheck-friendly means replacing softmax, which costs +6.8% at 2 layers and +19.8% at 8 — a divergence, not a tax a bigger model amortises.
the polynomial route is closedDoes the contract hold on hardware that isn't a Mac?
Yes — Intel x86 on two operating systems, and an NVIDIA L4 with TF32 left enabled. The NVIDIA operand bound of 2¹¹ was predicted from the Apple measurement and recorded before the hardware was available, then confirmed exactly. Qwen2.5-0.5B then produced byte-identical logits on all five machines.
pre-registered prediction confirmedWhat do you do about the bandwidth, then?
Audit one random layer, backed by a stake — always-on, and enough to make cheating negative-expected-value at 4.2% of the traffic. Where a conclusive ruling is wanted, bisection to the first divergent digest names the guilty layer with certainty at the same bandwidth, in 5 rounds and 1.9 KB. The two are complementary rather than competing.