# Verification taxonomy **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 specified `f`, `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: 1. **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. 2. **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. 3. **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". 4. **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: 1. **Which claims** (O/A/B/C/D/E) the evidence supports, using these labels. 2. **Which level** (L0–L6). 3. **Soundness error**, if L3 — as a number, per check and after `k` checks. 4. **Trust assumptions**, enumerated: who must be honest, which key must stay secret, which vendor must not be compromised, which cryptographic assumption must hold. 5. **`R`**, the cost ratio, with the native baseline measured on the same machine in the same run. 6. **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 `VERIFIED` status 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`.