Work versus output

Checkpoint: CP-011 Status: COMPLETE. Run 2026-09-01. Question: what can correctness verification not see, and does that gap actually cost the network money?

Result

Seven provider strategies against the strongest checker we have built (exact Freivalds over F_p, soundness 9.1 × 10^-13), n = 2048:

Every answer-changing cheat is caught — including the reduced-precision attack that defeated the floating-point checker in E009-pre. Exact arithmetic has no tolerance to hide in.

Exactly one strategy is accepted while doing materially less work: returning a cached correct answer. No checker of any strength can object to it, because the answer is right. It is a pricing bug, and it is closed by a hash-table lookup in the coordinator.

The other low-work strategy that passes is Strassen's algorithm, which is not an attack at all — it is a better algorithm producing the exactly correct result. A correctness 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.

The report

analysis.md answers the commissioned question — is there a purely software mechanism that can force a provider to perform substantial work, or does this require trusted hardware or economics? — with the literature checked first.

In brief: forcing useful work in software is not an open problem (Ball et al. 2017/2018; Komargodski–Weinstein 2025 achieve 1+o(1) overhead for matrix multiplication), but every construction rests on an unproven hardness conjecture — we have no unconditional superlinear lower bounds, and ω is still falling (< 2.371177). A 50+ scheme SoK concludes PoUW "is actually not as useful as expected". The direct ML analogue, Proof-of-Learning, was published and then broken by spoofing attacks. VDFs and proofs of sequential work do force expenditure, but by being unparallelisable and useless — the opposite of what a GPU compute market wants.

Claim C (work performed) is conditionally achievable in software. Claim D (physical resource expenditure) is not. And 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.

Files

Checkpoint CP-011

What can correctness verification not see — and does that gap actually cost the network money?

Where this question came from

E001, E003 and E009-pre all answered a correctness question: is the returned output right? A compute economy asks a different one: did the provider spend what it is billing us for? Those are not the same claim (Claim A versus Claims C and D in docs/verification-taxonomy.md), and this experiment is about the gap between them.

The original framing proposed for this work was:

"Can we design or verify a computation such that a provider cannot cheaply produce the correct output without performing substantial underlying work?"

We deliberately did not adopt that framing, for a reason worth recording before the experiment rather than after:

"Cannot cheaply produce" is a computational lower bound, and we cannot prove those. For matrix multiplication specifically, the true exponent ω is unknown and has been falling for fifty years (currently ω < 2.371177). Nobody can prove that an n×n product requires n³ work, or n^2.5, or anything above n². Any mechanism claiming "the provider must have done the work" therefore rests on an unproven hardness assumption, not on a theorem.

So we ask the decidable version instead, and treat the impossibility side as a literature question rather than an experimental one.

Hypotheses

H13a. Exact verification catches every strategy that changes the answer, including approximation shortcuts (low-rank, partial evaluation, reduced precision) — because approximation is a change to the answer, and exact arithmetic has no tolerance to hide in.

H13b. Exact verification catches no strategy that preserves the answer. Specifically:

• Strassen's algorithm produces the exactly correct product with strictly less arithmetic and will be accepted — correctly, because there is nothing wrong with it.
• A cached correct answer will be accepted with zero work performed.

H13c (the load-bearing one). The set of "accepted while doing materially less work" strategies contains only cases that are pricing problems, not verification problems — and are therefore fixable without cryptography.

What each outcome would mean

The framing this experiment is really testing

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

If Nodus prices jobs from the specification (model, tokens — both computable by the coordinator from data it already holds), a provider with a better algorithm earns more margin, exactly as in any other market. Strassen is the clean test case: it is indistinguishable from "laziness" to a correctness checker, and it is unambiguously something a compute market should want.

Implementation: implementation/adversaries.py.

The job

Compute C = A·B for n×n int8-valued operands (as in quantised inference). The honest reference is the textbook O(n³) product via BLAS; that is what the network is assumed to be billing for.

The verifier

Exact Freivalds over F_p, p = 1048573, k = 2 rounds — the mechanism from E003 variant D, soundness ≤ 9.1 × 10^-13, no tolerance, no tuning. We use the strongest checker we have built, so that anything which gets past it is a genuine limitation of correctness verification rather than of our implementation.

Provider strategies

Measurements

• Scalar multiplications, analytically. For Strassen with L levels down to a cutoff of m, this is 7^L · m³ against the naive n³.
• Wall time, measured.
• Exact correctness against the true product.
• Verifier verdict.

Two honesty notes

1. Wall time and arithmetic disagree for Strassen. Our Strassen does 67–77% of the multiplications but takes 1.6–2.5× the wall time, because it is Python recursion over numpy blocks competing against a decades-tuned BLAS. The arithmetic saving is real and is what the analytic column reports; production Strassen implementations do beat BLAS at large n, but ours does not, and we do not claim otherwise.
2. cheat-cached is measured as zero work by construction. It is not "cheating" in the arithmetic sense — it returns a genuinely correct answer. That is precisely why it is interesting.

Environment

Apple M5, 10 cores, 25.8 GB; NumPy 2.5.2 + Accelerate; n ∈ {1024, 2048}; single run per configuration.

Checkpoint CP-011. Status: complete. Date: 2026-09-01. Raw records: ../../benchmarks/results/013-work-vs-output.jsonl

This is the report requested at the end of Experiment 002's brief, answering:

Is there a purely software/cryptographic mechanism that can economically force a provider to perform substantial work, or does Proof of Resource Expenditure fundamentally require some form of trusted hardware, attestation, or economic mechanism?

Short answer, with the literature checked first as the charter requires:

Software mechanisms that force work exist and are real — but every one of them rests on an unproven hardness conjecture rather than a theorem, and none of them establishes physical resource expenditure. More importantly, our measurements suggest Nodus does not need them: exact correctness verification caught every cheating strategy we could construct except one, and that one is a pricing bug, not a verification failure.

---

1. Measured results

n = 2048, verifier = exact Freivalds over F_p, k = 2:

Identical pattern at n = 1024.

H13a confirmed. Every strategy that perturbs the answer is rejected — including cheat-precision, the reduced-precision attack that defeated the floating-point checker in E009-pre. Exact arithmetic has no tolerance to hide in, so approximation and correctness are the same question.

H13b confirmed. No strategy that preserves the answer is rejected, and there are exactly two of them: a better algorithm, and a cached result.

H13c confirmed, and it is the point. The "accepted with materially less work" column has one entry, and it is caching.

2. What the two accepted-with-less-work cases actually are

Strassen — not an attack, and the checker is right to accept it

Strassen's algorithm produced the exactly correct integer product using 67% of the multiplications. It passes every check we have, and it should.

This is the clarifying case. A correctness verifier cannot distinguish "did less arithmetic because it is cleverer" from "did less arithmetic because it is lazy", because at the level of the output there is no difference. Any mechanism that penalised Strassen would be penalising efficiency.

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

Under output-based pricing — where CU is derived from the job specification — this provider is simply a better supplier earning a better margin, exactly as in every other market. Under effort-based pricing it is a fraudster. The difference is entirely in the pricing rule, not in the cryptography.

(Caveat kept honest: our Strassen does 67% of the arithmetic but takes 2.45× the wall time, because Python recursion cannot compete with a tuned BLAS. The arithmetic saving is real; this implementation does not realise it. Production Strassen does beat BLAS at large n.)

Caching — a real exploit, and not a verification problem

A provider that has seen (A, B) before returns the stored C. It is correct, it passes, and it performed zero work. This is a genuine loss of revenue for honest providers and a genuine mispayment by the network.

But note what it is not: no correctness checker of any strength can object, because the answer is right. Improving the verifier is provably useless here.

The fixes are cheap and non-cryptographic:

1. Deduplicate on the input commitment. The coordinator already hashes inputs (v1's input_hash). If it has paid for (model, input) before, it should not pay full price again — it should serve its own cached result. Cost: a hash lookup.
2. Bind freshness where repetition is expected to be rare, so a replayed answer for a new job is impossible by construction.
3. Observe that at temperature > 0, or with any nonce in the prompt, exact input repetition is already vanishingly rare in practice.

The single surviving exploit against exact correctness verification is solved by a hash-table lookup in the coordinator.

3. Literature: is forcing work solved? (searched before concluding)

It is not an open problem, and it would have been wrong to treat it as one.

Proofs of work on useful problems exist. Ball, Rosen, Sabin and Vasudevan construct PoWs whose hardness reduces to Orthogonal Vectors, 3SUM and All-Pairs Shortest Paths — worst-case fine-grained assumptions — so that mining does useful computation (ePrint 2017/203; CRYPTO 2018).

And specifically for our problem. Komargodski and Weinstein, Proofs of Useful Work from Arbitrary Matrix Multiplication (ePrint 2025/685), give a PoUW for matrix multiplication with 1 + o(1) multiplicative overhead over naïve matmul — remarkably cheap, and directly on the primitive Nodus cares about.

So the honest answer to "can software force work" is yes, for suitable problems. But three qualifications decide whether it helps Nodus:

(a) The hardness is conjectural, not proven. Komargodski–Weinstein explicitly conjecture optimal security, reducing it to a new assumption about solving batches of low-rank random linear equations. Ball et al. rest on fine-grained complexity assumptions. This is not a defect of those papers — it is unavoidable. We have no unconditional superlinear lower bounds. For matrix multiplication the exponent ω is unknown and still falling: 2.371866 (2020) → 2.371552 → 2.371339 → < 2.371177 (2026). Nobody can prove a matmul requires more than n² work. "The provider must have expended the work" is therefore always a statement about a conjecture.

(b) The PoUW literature's own verdict is negative. Dikshit, Emami, Sedlmeir and Fridgen, SoK: Is Proof-of-Useful-Work Really Useful? (ePrint 2025/1814) survey more than 50 PoUW constructions, find "recurring shortcomings", and conclude:

"Our finding show that PoUW is actually not as useful as expected, since the economic and societal utility do not contribute to the security budget."

(c) The direct ML analogue was proposed and broken. Proof-of-Learning (Jia et al., IEEE S&P 2021) is exactly "prove you spent the compute to train this model". It was defeated by spoofing attacks that produce valid-looking proofs cheaply — Zhang et al., "Adversarial Examples" for Proof-of-Learning (arXiv:2108.09454), and Fang et al. (2023), who describe systemic vulnerabilities that depend on advances in understanding optimisation to fix.

And the mechanisms that genuinely do force expenditure force the wrong thing. Proofs of Sequential Work (Mahmoody–Moran–Vadhan 2013; Cohen–Pietrzak, EUROCRYPT 2018) and Verifiable Delay Functions (Boneh–Bonneau–Bünz–Fisch, CRYPTO 2018) prove that sequential time elapsed. They achieve this by being deliberately unparallelisable, and their work is deliberately useless. Nodus wants work that is massively parallel and useful. These are close to opposite requirements. Proofs of Space (Dziembowski–Faust–Kolmogorov–Pietrzak, CRYPTO 2015) prove storage, not compute.

4. Answering the question

Is there a purely software/cryptographic mechanism that can economically force a provider to perform substantial work?

Partially, and not in a form that helps here.

So the split in the brief is right, and the answer differs by row: Claim C (work performed) is conditionally achievable in software; Claim D (physical resource expenditure) is not. Hypothesis H5 survives.

5. But the more useful answer is that Nodus should not need it

The measured table in §1 is the argument. Against the strongest checker we have:

• every answer-changing cheat is caught, with an exact 9.1 × 10^-13 bound;
• the only answer-preserving exploit is caching, closed by a hash lookup;
• the remaining "shortcut" is a better algorithm, which a compute market should reward rather than police.

That leaves a design position that is cheaper and better than solving proof of expenditure:

Price the job, not the effort. Derive CU from the job specification — model and token counts, both computable by the coordinator from data it already holds — and verify only that the output is correct. Then a provider's efficiency is its own margin, caching is a dedup problem, and Claim D never enters the settlement path.

This is the same conclusion the v1 analysis reached from the opposite direction (docs/mvp-analysis.md §4): v1 currently settles on provider-reported token counts that the coordinator could simply recompute. Fixing that one line moves Nodus onto specification-based pricing, and the hard claim disappears rather than being solved.

6. Where Claim D genuinely still matters

Not everything is per-job settlement, and these cases are real:

These are the honest home of Stage 9/10 work, and they are a much smaller problem than "verify all inference expenditure".

7. What a malicious provider can still get away with

1. Caching, until dedup is deployed. The only measured hole.
2. Being efficient and billing the specification price. By design, and correctly so.
3. Sub-contracting the job to cheaper hardware.
4. Everything about capacity and availability claims (§6).
5. Attacks on the specification rather than the execution: if the job spec does not pin the quantisation scheme or numeric semantics, a provider can be "correct" with respect to a cheaper spec than the one intended. This is now the largest remaining verification-adjacent risk, and it is a specification problem, which is where E009-pre also landed.

8. Limitations

• Matrix multiplication only. A full inference pipeline has non-linearities, and "approximation" there may not be as cleanly answer-changing.
• Seven strategies. Absence of a successful attack in a hand-built catalogue is weak evidence of absence; a genuinely adversarial effort would try harder.
• Strassen is the only algorithmic shortcut tested. Fast-matmul methods below n^2.807 exist but are impractical at these sizes.
• The economic claim in §5 is an argument, not a measurement. Modelling the cost to Nodus of not solving expenditure — under output-based pricing, with a dedup rate drawn from real traffic — has not been done and is the obvious next quantitative step.
• The literature review is a first pass. SoK 2025/1814 and Komargodski– Weinstein 2025/685 have been read at abstract/conclusion level only; Ball et al. and the PoL attack papers have not been read in full.

1. Deploy the two cheap fixes this experiment justifies

Neither is research; both are findings with an obvious implementation.

• Specification-based metering. Derive CU from the job spec and the committed I/O rather than from provider-reported token counts (docs/mvp-analysis.md §4, coordinator/jobs.py:419-421). This is what puts Nodus on output-based pricing, which is the premise of the whole §5 argument.
• Job dedup on the input commitment. Closes the single measured exploit. A hash lookup against (model, model_version, input_hash); if the network has paid for it before, serve the stored result instead of paying again.

2. Quantify the argument in §5

The claim "Nodus does not need proof of expenditure" is currently an argument, not a measurement. Make it one:

• What fraction of real traffic is an exact repeat? (v1's job table can answer this directly, though n=14 is far too small — instrument and wait.)
• Under output-based pricing, what is the network's expected loss from all remaining exploits? If it is a fraction of a percent, the Claim-D branch closes on evidence.

3. Attack the specification, not the execution

Both this experiment and E009-pre landed on the same residual risk: a provider can be "correct" with respect to a cheaper specification than the one intended. If the job does not pin numeric semantics and quantisation, there is nothing to be correct about. Concretely:

• draft a minimal numeric contract for a job class (dtype, quantisation scheme, accumulation width, tolerance if any);
• measure how many honest backends can actually satisfy it;
• measure what it costs to check conformance.

This is now the most valuable open design question in the programme.

4. Finish the literature pass

Read in full rather than at abstract level:

• Komargodski & Weinstein, PoUW from Arbitrary Matrix Multiplication (2025/685) — 1+o(1) overhead on our exact primitive is remarkable, and if its conjecture is credible it may deserve an experiment of its own.
• Ball, Rosen, Sabin, Vasudevan (2017/203, CRYPTO 2018).
• Dikshit et al., SoK: Is PoUW Really Useful? (2025/1814) — read the economic model in full; it bears directly on how Nodus should price.
• Jia et al., Proof-of-Learning (S&P 2021) and the Zhang / Fang attacks.

5. Only then, Stage 9

The cases in analysis.md §6 — capacity claims, Sybil resistance, paying for availability — are where Claim D genuinely still bites, and they are a much smaller problem than "verify all inference expenditure". That is the honest scope for TEE/attestation work, and it should be scoped that way rather than as a general solution.

Deliberately not doing

• Building a PoUW for matmul. The literature has one with 1+o(1) overhead. Reimplementing it would be a re-derivation, and the SoK's economic critique suggests the result would not change our architecture.
• Chasing lower bounds. Not a research programme we can win.