Verification taxonomy
Claims O/A/B/C/D/E, levels L0–L6, and the mechanism matrix.
Status: living document. Last revised 2026-09-01.
The purpose of this document is to make it impossible to write a sloppy sentence about verification in this repository. Every claim in every experiment report must cite one of the labels defined here.
1. Claims
A verification mechanism produces evidence. Evidence supports specific claims. The claims are not interchangeable and almost no mechanism supports all of them.
Claim O — Origin
The artefact was produced by party P, was not modified, and is not a replay.
Mechanisms: MACs, digital signatures, nonces, transcript binding. This is a prerequisite, not an achievement. Nodus v1 has exactly this.
Claim A — Correctness
output = f(model, input)for the specifiedf,model,input.
Mechanisms: SNARK/STARK, interactive proofs, replication, spot checks.
Note that Claim A is only meaningful when f is well defined. For
floating-point neural inference on heterogeneous accelerators, f is not a
single function — it is a family of functions differing in rounding. Claim A
must therefore always be qualified: correct with respect to which reference
semantics, and within what tolerance?
Claim B — Execution
The provider actually ran the specified computation, on this occasion, to obtain this result.
Distinct from A: a provider can hold a correct output without executing anything (cache, collusion, precomputation). Cryptographic proofs of A do not imply B. Freshness/binding constructions (unpredictable inputs, challenge nonces inside the committed statement, timing bounds) are what speak to B.
Claim C — Work
The provider performed the claimed quantity and type of computational work.
This is what a resource-priced economy actually bills for. It is the claim most often silently conflated with A. Note that C is upper-bounded by the job specification, not by the provider's report: if the coordinator can derive the work from the spec plus the committed I/O, C becomes trivial; if not, C requires D.
Measured verdict (E013, CP-011): against exact verification, every answer-changing cheat is caught, and the only answer-preserving exploit is returning a cached correct result — a pricing problem, closed by deduplicating on the input commitment. A provider using a faster algorithm (Strassen) is accepted, correctly: at the level of the output there is no difference between "cleverer" and "lazier". A shortcut is only an attack if you are paying for effort rather than output.
Claim D — Physical resource usage
A specific physical machine consumed the claimed GPU-seconds, cycles, memory bandwidth, or energy.
The hardest claim. Nothing in pure cryptography establishes it: a proof is a mathematical object and carries no information about the hardware that produced it. Only hardware roots of trust, physically-observed side channels, or trusted measurement infrastructure can speak to D, and each of those is conditional on a trusted party. Default assumption: Claim D is not achievable trustlessly. (Hypothesis H5.)
Literature checked (E013, literature.md §5a), and the position stands with
one refinement. Software can force work — proofs of useful work exist,
including one for matrix multiplication at 1+o(1) overhead (Komargodski–
Weinstein 2025) — but every such construction rests on an unproven hardness
conjecture, because there are no unconditional superlinear lower bounds (ω
itself is unknown and still falling, currently < 2.371177). And forcing work is
still not evidence about a machine. So:
Claim C is conditionally achievable in software. Claim D is not.
The closest published attempt at expenditure-proof for ML — Proof-of-Learning (IEEE S&P 2021) — was broken by spoofing attacks.
Claim E — Useful computation
The provider performed the genuinely required work, rather than: returning a cached result, silently substituting a smaller/other model, skipping layers, taking an approximation shortcut, fabricating intermediate state, or precomputing the answer.
E is a conjunction, not a primitive. In practice
E ≈ A ∧ B ∧ (model binding) ∧ (freshness). Model binding — proving which
weights were used — is a separate cryptographic requirement (a commitment to
the weight tensor that is an input to the statement) and is missing from most
naive designs, including Nodus v1.
2. Evidence strength ladder
Ordered by how much trust is removed, not by cost. Cost is orthogonal and frequently inverted with respect to this ordering.
| Level | Name | What it rests on | Nodus example |
|---|---|---|---|
| L0 | Assertion | nothing | provider's self-reported duration_ms |
| L1 | Authenticated assertion | key secrecy | v1 HMAC receipt (Claim O only) |
| L2 | Corroborated assertion | ≥1 independent party honest | replication / cross-execution audit |
| L3 | Probabilistic verification | soundness error computable and adjustable by the verifier | Freivalds check, random segment audit |
| L4 | Hardware-rooted attestation | vendor + firmware + attestation service honest and unbroken | SGX/SEV-SNP/H100 CC quote |
| L5 | Cryptographic proof | standard computational assumptions | SNARK / STARK |
| L6 | Unconditional | information-theoretic | rarely reachable for this workload class |
Three things follow that are easy to get wrong:
- L3 is not weaker than L5 for a rational adversary. L5 bounds the adversary's success by ~2^-100. L3 bounds it by a number we choose, e.g. 2^-40, at vastly lower cost. Against an economically motivated attacker, the relevant comparison is expected profit, not soundness error. A 1-in-10^12 chance of stealing 0.01 CC is not an attack.
- L4 is not on the same axis as L5. A TEE is not a weak proof; it is a different trust assumption. Composing them (L4 ∧ L5) is not redundant.
- No level implies Claim D. L4 comes closest and still only asserts "code ran inside an enclave the vendor vouches for", not "this many GPU-seconds were consumed".
- L3 mechanisms inherit their threshold from the honest population, not from the adversary. E009-pre measured honest CPU-vs-GPU divergence at within 3.7× of a real precision cheat, which leaves no settable threshold. A probabilistic check is only as sharp as the agreement among honest participants, and that agreement is an empirical property of the network's hardware — not a parameter the protocol designer gets to choose.
3. Mechanism × claim matrix
Y = supports the claim. ~ = supports it partially or under extra conditions.
N = does not support it. ? = UNKNOWN, to be resolved by experiment.
| Mechanism | Level | O | A | B | C | D | E | R (cost/native) |
|---|---|---|---|---|---|---|---|---|
| HMAC receipt (Nodus v1) | L1 | Y | N | N | N | N | N | ~0 |
| Full re-execution | L2 | – | ~ | N | ~ | N | ~ | ~1.0 |
| n-of-m replication + vote | L2 | – | ~ | N | ~ | N | ~ | n |
| Random spot-check audit | L3 | – | ~ | ~ | ~ | N | ~ | audit rate × 1.0 |
| Freivalds matmul check (exact arith.) | L3 | – | Y | N | N | N | N | 0.023 MEASURED (E003, n=8192) |
| Freivalds matmul check (float, heterogeneous) | L3 | – | ~ | N | N | N | N | 0.023, but detects only gross error (E009-pre) |
| Interactive proof (GKR/sumcheck) | L3/L5 | – | Y | N | N | N | ~ | 792 B comms for a 2-layer 2048² chain (E019); zero saving once LUT non-linearities break the chain |
| General zkVM (SP1/RISC0) | L5 | – | Y | N | ~ | N | ~ | R_verify 34 · R_prove 7e4 MEASURED (E001) |
| Specialised ZKML (e.g. ZIP) | L5 | – | Y | N | ~ | N | ~ | ~10^7 measured (see literature) |
| TEE attestation | L4 | Y | ~ | Y | ~ | ~ | ~ | small, but ? |
| Hardware exec receipt | L4 | Y | ~ | Y | Y | ~ | ~ | SPECULATIVE |
| Commit-to-weights + any of above | – | – | – | – | – | – | +binding | additive |
| Challenge nonce in statement | – | – | – | +B | – | – | +freshness | ~0 |
Reading of the matrix, stated as a claim to be tested rather than a conclusion: the D column is empty except under trusted hardware, and the cheapest useful columns are the L3 row block.
Evidence as of 2026-09-01 (E001, E003): the L3 row block is not merely
cheaper, it is cheaper by nine orders of magnitude on R_verify than the L5
row block for the same Claim A — 0.023 versus 34 at best, and versus 8.2 × 10^7
for a small job. The R column is doing more work in this table than the claim
columns are. That said, the two rows are not substitutes: the L5 row supports
third-party verification and weight privacy, and the L3 row does not, because
the Freivalds verifier must hold the operands.
4. Required qualifiers
When any experiment in this repo reports a result, it must state:
- Which claims (O/A/B/C/D/E) the evidence supports, using these labels.
- Which level (L0–L6).
- Soundness error, if L3 — as a number, per check and after
kchecks. - Trust assumptions, enumerated: who must be honest, which key must stay secret, which vendor must not be compromised, which cryptographic assumption must hold.
R, the cost ratio, with the native baseline measured on the same machine in the same run.- What a malicious provider can still get away with. Mandatory section.
5. Vocabulary rules
- "Proof" is reserved for L5/L6. A random audit is a check, not a proof.
- "Verified" without a claim label is meaningless; v1's
VERIFIEDstatus means Claim O verified and should be read that way. - "Trustless" is not used in this repository. Everything has a trust set; state it.
- "Proof of useful computation" is not used unless Claims A, B and E are all supported, with model binding.
- Numbers are labelled MEASURED, DERIVED, DECLARED, SPECULATIVE,
or UNKNOWN, following the convention already established in
../nodus/PAPER_BRIEF.md.