Research log

The findings in the order they were discovered, which is not the order they make sense in. ../README.md presents the conclusions; this file keeps the route, including the wrong turns.

Reading it in sequence shows the programme changing its mind four times: a cryptographic answer abandoned on cost, a probabilistic one falsified by hardware, a contract that dissolved the problem, and a bandwidth bill that arrived after all of it and reopened the design.

---

Headline finding: the same claim, nine orders of magnitude apart

Both of the mechanisms below establish Claim A (the output is correct). Both were measured on the same machine in the same week, each against a native baseline measured in the same run.

The difference is not implementation quality. A zkVM proves a RISC-V execution trace and pays for every load, branch and index computation; Freivalds exploits the algebraic structure of the statement and makes the verifier do a small amount of work instead. Verifying an 8192×8192 matrix product costs 2.3% of recomputing it, with no cryptographic assumptions at all.

…and the catch, also measured

Freivalds' clean guarantee assumes exact arithmetic. In floating point it degrades to an approximate-correctness check with a tolerance, and E009-pre measured what that tolerance has to be in a heterogeneous network:

A 2,800× separation is a threshold anyone can set. A 3.7× separation is not. The cause is the device: mlx-cpu-f32 and mlx-gpu-f32 — identical library, identical dtype, one line of difference — diverge by 765–3,069×, with a constant relative error that is the signature of operand rounding rather than accumulation. A backend advertising float32 may not be computing in float32.

This falsified a conclusion we had written in E003 the same day, and it points somewhere unexpected:

The binding constraint on cheap verification is not its cost. It is the numerical agreement among honest providers. The decisive design lever may therefore be specifying arithmetic — mandating exact or quantised-integer semantics — rather than choosing a proof system.

What survives: the check still catches gross cheating (fabricated output, substituted model, skipped layers — all 10^-2–10^0 relative error), which is to say it catches the cheats that actually save a provider money.

And then the problem dissolved

E014 re-ran that comparison on integer operands rather than real-valued ones:

The GPU's imprecision was never about the GPU. It was about representing real numbers. Given integers in range, the same hardware that diverged by 1,500× returns the bit-exact product.

So the expected supply/security trade-off does not exist: the strictest contract admits every honest backend we tested, CPU and GPU alike, while separating cheats without bound. The heterogeneity problem did not need a cleverer threshold — it needed different arithmetic. Deliverable: docs/numeric-contract.md, draft NC-0.1.

Which held for a whole layer

E015 put a transformer-shaped layer — three matmuls, softmax, GELU, layernorm, requantisation — under that contract. Output was bit-identical on numpy-CPU, MLX-CPU and MLX-GPU at every shape tested.

The move that makes it work is specification, not arithmetic: non-linearities are specified as integer lookup tables rather than as formulas. A gather is memory indexing, so there is nothing to round — divergence becomes structurally impossible rather than merely unlikely.

Verification splits cleanly, and yields a design rule:

R_verify ≈ the fraction of the layer that is non-linear.

We predicted under 10% and measured 47–96% — most of which is our own numpy overhead (our Freivalds runs 112× slower than its own arithmetic for want of a BLAS path). The structure is confirmed; the absolute number is not yet established, and the largest unmodelled cost is bandwidth — the verifier needs the layer's intermediate tensors.

And it holds on a transformer, doing generation

E018 put a real char-level transformer — attention, softmax, residuals, layernorm, GELU — under the contract and generated text. 10 prompts × 300 tokens:

One honest float pair in ten diverged. That is the number Nodus v1 has needed since it was built — its replication check compares output hashes on evidence of n=1, against a simulated node. A 10% false-positive rate means output-hash replication cannot be used for enforcement: you would slash one honest provider in ten. Under the contract the rate is zero, by construction.

Quality cost: +1.4% perplexity over ordinary quantisation — materially more than the ~0 on MNIST, because a classifier's argmax absorbs perturbations and a language model's perplexity does not.

And the contract had a real bug, which the experiment found. NC-3 bounded the accumulator at 2^24. MLX's Metal matmul turns out to be exact only up to operands of 2^11, regardless of accumulator size — 13 bits tighter, and the binding constraint all along. Every earlier experiment satisfied it by accident (int8 operands are ≤127); attention probabilities at 2^15 were the first to exceed it, and CPU/GPU generation silently diverged at token 102. Fixed as clause NC-3b, now asserted rather than assumed.

A numeric contract is only as good as the quantity it bounds, and the binding constraint is backend-specific.

And it holds on a real model

E023 ran the contract on Qwen2.5-0.5B — 24 layers, vocab 151,936, GQA, RMSNorm, SwiGLU, RoPE — the model Nodus v1 actually serves, on wikitext-2.

Five backends produced byte-identical logits — Apple ARM CPU, Apple Metal GPU, two Intel x86 CPUs on different operating systems, and an NVIDIA L4 with TF32 enabled — with every next-token prediction matching. Two CPU vendors, two GPU vendors, three OSes, three Python versions.

TF32 was left on deliberately: int8 operands sit four bits inside NC-3b's 2^11 bound, so the reduced-precision tensor-core path cannot lose anything. The contract never asks a provider to cripple their hardware.

It also found a defect only a real model could reveal. Measured with float accumulation, so this is about quantisation granularity alone:

Per-tensor quantisation destroys the model. That clause was written from a 2-layer toy where it was harmless. The contract is now NC-0.5.

Six rounds of implementation fixes took the integer path from +47.6% to +10.3% perplexity, and three of them were the same mistake: int8 is a storage convention, not the contract's limit. NC-3b permits 2^11, and every place we capped at 127 was discarding four bits for free.

Measured like for like, the cost decomposes cleanly: quantisation itself costs +6.9%, and full integer determinism adds +3.5% on top (float 23.27 → per-channel int8 with float accumulation 24.88 → contract 25.76).

(Superseded by E025 below: those were point estimates from 4–6 chunks, and at that sample size the interval contains zero. Paired over 120 chunks the costs are +6.67% [5.95, 7.40] and +2.43% [1.63, 3.23].)

That +3.5% is plausibly close to intrinsic. A float-accumulation pipeline quantises matmul inputs and keeps accumulators exact between steps; a fully-integer one cannot, so it has more rounding boundaries by construction.

The protocol that fixes the bandwidth — and doesn't fit

E019 implemented the sumcheck interactive proof. On a two-layer chain of 2048² matmuls it replaces a 16.8 MB intermediate with a 792-byte transcript — 21,183×, and improving with scale because communication grows logarithmically while the data it replaces grows quadratically.

On our transformer layer it saves nothing. All three matmul outputs — 49.1 MB, exactly E016's figure — feed lookup-table non-linearities that the verifier checks by recomputation. The chain breaks at the first non-linearity, and there is one after every matmul.

NC-9 makes non-linearities lookup tables because a gather has no arithmetic and so cannot diverge across backends. A sumcheck passes only through low-degree arithmetic. The property that buys determinism is the property that blocks the proof.

That also explains SafetyNets' restriction to quadratic activations, which had looked like an arbitrary compromise: y = x² is arithmetic, so the chain passes through it. They changed the model because the protocol demanded it.

And the price of fixing it is entirely in attention

E020 asked the obvious follow-up: if our lookup tables block the proof, what does changing the model cost?

Replacing GELU with x² is free. SafetyNets' famous activation restriction — the thing that looks like the painful compromise — costs nothing here.

Replacing softmax is what costs, and it is the change that actually matters. E019 had framed this as "adopt quadratic activations"; that was incomplete. SafetyNets' networks had no attention, and their only softmax was the final classification layer, which they explicitly exclude from the proof. A transformer cannot make that exclusion.

So the trade is now measured: roughly three extra points of perplexity buys a ~60,000× bandwidth reduction — the difference, on E016's cost model, between a scheme that loses money and one that is free. Both architectures are laid out in docs/architecture.md §6.

And that caveat was right — E020b measured it at scale:

Softmax improves with depth. Squared attention stops improving and then regresses. The gap is a divergence, not a fixed tax a larger model amortises.

Decision: the polynomial route is closed. Nodus keeps the model and pays the bandwidth — NC-0.3 contract + one-random-layer audit + a stake equal to the job's compute value. Works on an unmodified transformer, +1.4% perplexity, 39% of the cost of re-execution at 32 layers.

This also says something about SafetyNets: its quadratic-activation restriction is usually read as a dated compromise, but it looks load-bearing. Their networks were CNNs with no attention to lose. A transformer's inductive bias lives in exactly the operation a sumcheck cannot pass through.

And the bill on all of it, paid

We had been recommending the network switch to exact integer arithmetic without ever measuring what that costs in answer quality. E017 measured it. The number that matters is not "integer vs float" — ordinary quantisation is already integer and known to work — but the extra cost of being integer end to end, with no float step anywhere to reintroduce cross-backend divergence:

At 8 bits, full determinism is free within measurement noise. CPU and Metal GPU produced bit-identical logits on all 10,000 test images. It starts to bite at 4 bits, which gives a usable precision floor rather than a blanket claim.

That closes the last blocking unknown on the contract — and it is the direct answer to EigenAI's stated future work, "portable numeric normalization to enable heterogeneous verifier sets". Caveat we are not hiding: MNIST is an easy task, and no transformer or generation workload has been tested.

Then the bill we hadn't counted

E016 measured the cost of getting the verifier its data. It dominates by three to five orders of magnitude.

Every configuration loses. The earlier R_verify figures are compute ratios resting on an assumption we hadn't stated — the verifier already holds what it needs. True for one matmul the coordinator owns; false inside a pipeline.

The rescue: audit one random layer instead of every layer. Bandwidth stays flat while compute saved scales with depth, so at 32 layers on cheap egress verification costs 39% of re-executing. Soundness falls to 1/L — and the required stake falls out cleanly, because the m and L cancel:

A stake equal to the job's compute value makes layer-skipping negative-expected-value, at any depth and any level of greed.

This also promotes interactive proofs (GKR / SafetyNets) from interesting to the known answer: polylogarithmic communication is precisely what this cost demands. We have not measured them yet.

The fix, measured the same day

Every part of that failure traces to one cause: inexact arithmetic forces a tolerance, and the tolerance is the attacker's budget. Running the same check over a prime field on quantised-integer operands removes it:

Exact arithmetic costs 2× and buys back the entire guarantee — R_verify moves from 2.3% to 4.6% of the computation being policed, and the mechanism stops having a security parameter an attacker can aim at. It detects 64 entries off by one (≈1 part in 10^8), which no float tolerance can see.

That yields the programme's first concrete architectural recommendation: mandate quantised-integer semantics for verifiable job classes. It is a constraint on the workload specification, arrived at from a verification requirement — which is what hypothesis H7 predicts. Its price is the accuracy cost of quantised inference, which we have not yet measured.

Experiment 001 in detail

Proving y = 3x + 5 in a general-purpose zkVM on an Apple M5:

Proving ten thousand of those statements costs the same 11 s. The cost is almost entirely a fixed per-proof charge, not a charge for the work — which means the interesting economic question is not "how expensive is ZK" but "how much work can you amortise a proof over". Full analysis: experiments/001-simple-arithmetic/analysis.md.

---

And the question underneath all of it

Nodus does not pay for correct answers. It pays for compute units. Those are different things, and almost all of the verifiable-computation literature addresses the first.

Experiment 013 ran seven provider strategies against our strongest checker. Every cheat that changes the answer is rejected. Exactly one strategy is accepted while doing materially less work — returning a cached correct answer — and no checker of any strength can object to it, because the answer is right. It is a pricing bug, closed by a hash lookup.

The other low-work strategy that passes is Strassen's algorithm: 67% of the arithmetic, exactly correct, accepted. Correctly accepted — a verifier cannot tell "cleverer" from "lazier", because at the level of the output there is no difference.

A shortcut is only an attack if you are paying for effort rather than output.

Literature checked before concluding: forcing useful work in software is not an open problem (there is a proof-of-useful-work for matrix multiplication at 1+o(1) overhead), but every such construction rests on an unproven hardness conjecture — we have no unconditional superlinear lower bounds, and ω is still falling. A 50-scheme SoK concludes proof-of-useful-work "is actually not as useful as expected". Proof-of-Learning, the direct ML analogue, was published and then broken.

Claim C (work performed) is conditionally achievable in software. Claim D (physical resource expenditure) is not. On our evidence Nodus should not need either: price the job from its specification, verify the output, dedup repeats, and let efficient providers keep their margin.

And the audit design is now a working protocol

E024 builds what E016 derived — Merkle commitment, uniform post-commitment challenge, opening, recomputation — and runs it against Qwen2.5-0.5B.

Building it corrected the paper design twice. The layer's output never needs transmitting — the verifier recomputes it and checks its own digest against the root, which halves the opening and is strictly more secure, because the provider never gets to say what the output was. And layer 0 is free: its input is the embedding the verifier already derives, so the opening is two Merkle paths and nothing else — 160 bytes.

It is not a proof, and shouldn't be called one: a single-layer cheat escapes with probability 1 − 1/L. The defence is the stake, not the probability.

The one metric

        cost of obtaining trustworthy evidence
  R  =  ──────────────────────────────────────
             cost of the native computation

with R_verify — the verifier's share — treated as decisive, because the verifier always has the option of simply re-running the job (R_verify = 1). Any mechanism above that line has to justify itself with something re-execution cannot provide: succinctness for a third party, privacy of the weights, or tolerance of non-determinism.

Every experiment reports R alongside a mandatory statement of what the evidence actually proves and what a malicious provider can still get away with.

---

And then we put error bars on the headline

E025 went back to the accuracy claim with the question a reviewer asks first: how do you know?

E023's "+3.5% for determinism" was a difference of two point estimates from 4–6 chunks. Re-measured over 120 paired chunks — every pipeline seeing identical tokens, intervals by bootstrap over chunks:

Two things came out of it, and the second matters more.

The number was wrong in our favour: +3.5% → +2.43%, with the old estimate outside the new interval.

And the old evidence could not have supported it. Resampling at five chunks gives [−1.36%, +6.47%] — an interval containing zero. E023's conclusion was right and its evidence did not establish it, which are different things, and the difference is invisible unless you go and check.

The design lesson is the pairing. Absolute perplexity here ranges from 8.6 to 43.3 across chunks — a 5× spread against effects of a few percent — so an unpaired study would have needed an enormous sample to see anything. Because every pipeline sees the same chunks, chunk difficulty cancels, and the interval on the gap is 1.6 points wide against ~5 on either endpoint.

One nuance worth keeping: the determinism gap holds its expected sign in only 83 of 120 chunks. The contract is worse on average by a little, not worse on every input — which is what a small rounding difference should look like.

And the prover turned out not to be the problem

E026 went after the last unquantified number in the paper: what the sumcheck prover pays. E019 could not measure it, because its sumcheck() runs both parties in one loop.

First answer: 36.1% at n = 4096. That looked like a second reason sumcheck does not transfer to transformers, on top of the bandwidth one.

It was wrong, and the breakdown said so. Two thirds of the cost was forming the multilinear extensions, so we looked at why. numpy has no BLAS path for int64, so the extension products were running at 733× the per-element cost of a float64 multiply-add. And two of the three field reductions were being applied to operands that were already residues, because NC-3b bounds them at 2^11 and the prime is 2^25.

Fixing both: 3.5× faster, bit-identical output, 10.4% at n = 4096, scaling as n^−0.92 against a predicted n^−1, reaching 5% by n ≈ 8,800.

The sumcheck rounds are 0.5% of the prover's overhead. The protocol is free. Everything else is the multilinear extensions and getting into the field, split about evenly.

Two things came out of this. The paper got stronger by losing an argument: the prover is not what blocks sumcheck for transformers, so the non-linearity structure is the only obstacle, which is a cleaner and more falsifiable claim.

And for the second time in three experiments, a number that looked settled was a measurement of our own code rather than of the thing we meant to measure. E017 taught this once, E025 taught it again, and E026 makes it three. It is now the default assumption.

Also falsified along the way: verification costs more than simply recomputing a single matmul at every size up to n = 2048, crossing below only at 4096. Sumcheck's advantage is bandwidth, not compute.

And then the audit got a conclusive sibling

E024's audit catches a single-layer cheat 4.2% of the time and leans on the stake. The economics are sound, but the verdict is never "this provider cheated", only "cheating loses money".

E027 borrows Arbitrum's fraud proof. Two parties who disagree binary-search to the first layer where their committed digests differ; an arbiter recomputes that one layer and rules.

Same bandwidth, same arbiter cost, conclusive instead of probabilistic. The extra cost is entirely the challenger's re-execution, which is the same trade Arbitrum makes: full work off-chain so the arbiter does O(1).

The hypothesis worth worrying about was H5 — does the search land on the layer that was actually cheated, or merely on the first place the digests happen to diverge? Blaming the wrong layer would mean slashing honest work.

24 of 24 correct, and the reason is the contract again. Under exact integer semantics a perturbation propagates to every later layer instead of being rounded away, so the first divergence is the cheat. The exactness that makes heterogeneous verification possible is also what makes the fraud proof point at the right layer.

Both properties also scale the right way: rounds grow as log2(L) while the arbiter's share is 1/L, so a deeper model makes adjudication cheaper.