# AI verification proposal

A proposal built with the Proposal Explorer of the AI Verification Tech Map (https://trustbutveri.fyi/), from its records of 2026-10-08. Interactive version: https://trustbutveri.fyi/explorer/?mechanisms=M-0003,M-0002&implementations=M-0002:I-0012

How to read it: a claim is something one party wants to verify about another's AI hardware or software. A mechanism is a general technique for verifying claims; it is "aimed at" a claim when that is its direct purpose, and "supporting" when it contributes without being aimed at it. A claim is addressed when a mechanism in the proposal is aimed at it and is not excluded by the filters; addressed does not mean verified, so check that mechanism's readiness and open flaws. Readiness levels R0 to R4 describe one record's public evidence for its assessed use and are never combined. Definitions: https://trustbutveri.fyi/about/methodology/ (roles, properties and flaws) and https://trustbutveri.fyi/about/readiness/ (readiness levels).

## Filters

Filters apply to mechanisms only and describe the setting the proposal is for.

None set. Every mechanism on the map was available.

## Overview

One row per mechanism, read from its record. Open flaws: critical / significant / minor. The last three columns are the editors' reading of what the verifier sees.

| Mechanism | Readiness | Prover | Attack testing | Hardware | Open flaws | Weights | Inputs and outputs | Training data |
| --- | --- | --- | --- | --- | --- | --- | --- | --- |
| Whole-workload recomputation (reproducible packets) | R1 | Adversarial | None | Retrofit device | 0 / 2 / 0 | depends | depends | depends |
| Deterministic and bit-exact inference / Low-trust AI compute verification system overview | R1 | Adversarial | Analysis | Retrofit device | 0 / 2 / 1 | unspecified | unspecified | unspecified |

## Claims

No claims chosen.

## Mechanisms

### Whole-workload recomputation (reproducible packets)

Organizing all AI workloads in a facility into discrete, reproducible units, so that a verifier can recompute a random sample and check each one. ([Whole-workload recomputation (reproducible packets)](https://trustbutveri.fyi/mechanisms/reproducible-computation-packets/))

- Assessment: mechanism family.
- Readiness: R1 Proposed, assessed for recomputing whole workloads to show a cluster runs only declared inference.
- Claims in this proposal: none of them.
- Threat model: adversarial prover. Hardware: retrofit device. Prover cooperation: required. Attack testing: none. Category: Isolation & system architectures.
- What the verifier sees: model weights depends; inputs and outputs depends; training data depends. Recomputing sampled units needs weights and sampled inputs or training data inside the checking environment. The design depends on securing that environment; disclosure depends on its confidentiality boundary.

### Deterministic and bit-exact inference

A retrofittable reference design in which network taps commit to all facility traffic, and air-gapped, independently sourced checkers later re-run randomly challenged records. ([Deterministic and bit-exact inference](https://trustbutveri.fyi/mechanisms/deterministic-inference/))

- Assessment: selected implementation [Low-trust AI compute verification system overview](https://trustbutveri.fyi/implementations/low-trust-compute-verification-system-overview/).
- Readiness: R1 Proposed, assessed for screening challenged records to show declared inference compute is not training.
- Claims in this proposal: none of them.
- Threat model: adversarial prover. Hardware: retrofit device. Prover cooperation: required. Attack testing: analysis. Category: Isolation & system architectures.
- What the verifier sees: model weights unspecified; inputs and outputs unspecified; training data unspecified. This Explorer has no asset-specific exposure assessment for this implementation. Check its source and deployment assumptions.


## Properties

**Built for an adversarial prover**

- Whole-workload recomputation (reproducible packets)
- Deterministic and bit-exact inference


## Attack testing

Published attempts to break a system, including those that found failures. Testing history does not establish that open flaws are resolved.

**Testing history**

- Deterministic and bit-exact inference / Low-trust AI compute verification system overview: Analysis


## Limits

**Open significant flaws**

- Spare compute is outside the scheme (theoretical argument, in Whole-workload recomputation (reproducible packets); https://trustbutveri.fyi/mechanisms/reproducible-computation-packets/#flaw-1) [1][2]. The plan states that it does not verify that spare compute is not used for unapproved workloads, because this seems very challenging. Recomputation checks the correctness of declared work, not its completeness.

  Related mechanism: Proofs of useful work for capacity accounting (R1, not in the proposal). Proposed as one input to accounting for spare capacity on declared hardware.
- Non-compliant work could be encoded inside compliant-looking packets (theoretical argument, in Whole-workload recomputation (reproducible packets); https://trustbutveri.fyi/mechanisms/reproducible-computation-packets/#flaw-2) [1]. The plan notes that an AI company might try to encode a non-compliant workload inside a workload that looks compliant on the surface.
- Mismatches cannot be attributed to cheating or error (theoretical argument, in Low-trust AI compute verification system overview; https://trustbutveri.fyi/implementations/low-trust-compute-verification-system-overview/#flaw-1) [7]. A failed hash or replay does not show whether it came from an evasion attempt, a random bit flip or an evaluation error. The author notes that if detected anomalies can plausibly be waved off as malfunctions, deterrence becomes less effective, so the parties need an agreed escalation procedure that ends in attribution.
- Inspector agents may be manipulable (open question, in Low-trust AI compute verification system overview; https://trustbutveri.fyi/implementations/low-trust-compute-verification-system-overview/#flaw-3) [7]. Automated compliance screening with LLM-based inspector agents must resist prompt-injection attacks. Adversarially trained systems might hide malicious actions with steganography, which makes backdoor detection an open problem.

**Family finding context**

- Context for Low-trust AI compute verification system overview; applicability depends on the finding's scope. Some kernels remain genuinely nondeterministic (open question, in Deterministic and bit-exact inference; https://trustbutveri.fyi/mechanisms/deterministic-inference/#flaw-1) [9]. The bit-exact work separates kernels that are deterministic but not batch-invariant from truly nondeterministic ones that use atomic functions. Some integer de-quantization kernels use atomic additions and remain nondeterministic, so exact replay needs backends that avoid them.
- Context for Low-trust AI compute verification system overview; applicability depends on the finding's scope. Cross-hardware replay relies on reverse-engineered, closed behaviour (open question, in Deterministic and bit-exact inference; https://trustbutveri.fyi/mechanisms/deterministic-inference/#flaw-2) [9][10]. Emulating one GPU's rounding on another requires reverse-engineering tensor-core arithmetic and modelling proprietary kernel choices. Hawkeye covers a subset of NVIDIA architectures and states that attention and other higher-level operations need further reverse engineering. For the bit-exact emulator, a proprietary Hopper kernel family is an open edge case.

**Open minor flaws**

- Deliberate faults leak a bit each (theoretical argument, in Low-trust AI compute verification system overview; https://trustbutveri.fyi/implementations/low-trust-compute-verification-system-overview/#flaw-2) [7]. A malicious device can leak one bit by deliberately outputting a wrong result, which blocks a disclosure when the cross-comparison fails. The design therefore needs a pre-agreed budget of tolerated faults.

**Not yet demonstrated**

- Whole-workload recomputation (reproducible packets): R1 Proposed, assessed for recomputing whole workloads to show a cluster runs only declared inference
- Deterministic and bit-exact inference: R1 Proposed, assessed for screening challenged records to show declared inference compute is not training


## Possible additions

Mechanisms on the map, not in the proposal, that the records connect to an unaddressed or partly addressed claim, an open flaw or a dependency. Pointers, not recommendations: each brings its own readiness level and flaws, and none is claimed to close a flaw.

- **Proofs of useful work for capacity accounting** (R1 Proposed, assessed for bounding the spare capacity of declared hardware that could run training)
  - Bears on the open significant flaw "Spare compute is outside the scheme" in Whole-workload recomputation (reproducible packets). Proposed as one input to accounting for spare capacity on declared hardware.
- **Tamper evidence for verifier devices** (R2 Demonstrated, assessed for detecting probing of proposed verifier hardware, using server and electronics prototypes as evidence)
  - Deterministic and bit-exact inference waits on it: Tamper-evident, rapidly mass-manufacturable and retrofittable enclosures for side-channel defence are an open research question, and physical security against covert communication in every monitored data centre is challenging.
- **Timed challenge-response and memory-occupation challenges** (R2 Demonstrated, assessed for detecting whether a GPU is doing other work)
  - Deterministic and bit-exact inference waits on it: Distinguishing one server's DRAM contents from another's by challenge-response timing, and a general challenge-response protocol for diverse data types, are open.
- **Network taps and certifiers** (R1 Proposed, assessed for committing a complete record of cluster traffic, so declared inference can be checked)
  - Whole-workload recomputation (reproducible packets) waits on it: All traffic must reach the recomputation server via network taps, and the server's integrity is critical.
  - Deterministic and bit-exact inference waits on it: Empirical feasibility of passive optical splitting at 53–112 GBaud under realistic conditions is an open question.
- **Side-channel suppression for isolated facilities** (R1 Proposed, assessed for bounding physical covert channels out of a verified enclosure)
  - Deterministic and bit-exact inference waits on it: A mass-manufacturable, good-enough side-channel defence, particularly power-line filtering, has not been constructed or red-teamed.


## Dependencies

**Missing prerequisites**

- Network taps and certifiers (R1 Proposed, assessed for committing a complete record of cluster traffic, so declared inference can be checked), needed by Whole-workload recomputation (reproducible packets) and Deterministic and bit-exact inference

**Shared foundations**

- Network taps and certifiers, relied on by Whole-workload recomputation (reproducible packets) and Deterministic and bit-exact inference

**Blockers**

- Whole-workload recomputation (reproducible packets): Workloads are not reproducible by default, and achieving reproducibility may cost performance. (performance & compatibility; waits on Deterministic and bit-exact inference) [1]
- Whole-workload recomputation (reproducible packets): Network packets are not individually reproducible by default; making them so may need considerable software, firmware and hardware work. Amodo rates this 'not on track'. (performance & compatibility) [4]
- Whole-workload recomputation (reproducible packets): All traffic must reach the recomputation server via network taps, and the server's integrity is critical. (hardware trust; waits on Network taps and certifiers) [1][4]
- Whole-workload recomputation (reproducible packets): Recomputing training steps needs checkpoints: writing one at every step would cost more than 100% overhead, so Amodo's design needs a spare data-parallel replica that tracks the weights instead. (performance & compatibility) [2]
- Deterministic and bit-exact inference: Empirical feasibility of passive optical splitting at 53–112 GBaud under realistic conditions is an open question. (performance & compatibility; waits on Network taps and certifiers) [7]
- Deterministic and bit-exact inference: Exact replay needs complete hardware and software metadata, and the tolerable slowdown from emulation is an open question. (performance & compatibility; waits on Deterministic and bit-exact inference) [7]
- Deterministic and bit-exact inference: Tamper-evident, rapidly mass-manufacturable and retrofittable enclosures for side-channel defence are an open research question, and physical security against covert communication in every monitored data centre is challenging. (hardware trust; waits on Tamper evidence for verifier devices) [7]
- Deterministic and bit-exact inference: A mass-manufacturable, good-enough side-channel defence, particularly power-line filtering, has not been constructed or red-teamed. (coverage & hidden compute; waits on Side-channel suppression for isolated facilities) [7]
- Deterministic and bit-exact inference: Distinguishing one server's DRAM contents from another's by challenge-response timing, and a general challenge-response protocol for diverse data types, are open. (coverage & hidden compute; waits on Timed challenge-response and memory-occupation challenges) [7]
- Deterministic and bit-exact inference: The threat model is under-developed and needs input from cybersecurity and AI threat-modelling experts. (adversarial validation) [7]


## What the verifier sees

- Model weights: shown by none; depends on the design for Whole-workload recomputation (reproducible packets); hidden by none; not involved in none; unspecified for Deterministic and bit-exact inference.
- Inputs and outputs: shown by none; depends on the design for Whole-workload recomputation (reproducible packets); hidden by none; not involved in none; unspecified for Deterministic and bit-exact inference.
- Training data: shown by none; depends on the design for Whole-workload recomputation (reproducible packets); hidden by none; not involved in none; unspecified for Deterministic and bit-exact inference.

## Implementations

- Whole-workload recomputation (reproducible packets): [AI 2040 inference-only verification stack](https://trustbutveri.fyi/implementations/ai-2040-inference-only-verification-plan/) (R1, proposed architecture)
- Deterministic and bit-exact inference: [Batch-invariant inference kernels (Thinking Machines)](https://trustbutveri.fyi/implementations/batch-invariant-inference-kernels/) (R2, open-source project); [Verde and RepOps (Gensyn)](https://trustbutveri.fyi/implementations/gensyn-verde-repops/) (R3, product); [Low-trust AI compute verification system overview](https://trustbutveri.fyi/implementations/low-trust-compute-verification-system-overview/) (R1, proposed architecture)

## Sources

1. Verification Plan, R. Dean (2026). https://ai-2040.com/supplements/verification-plan
2. Example Schemes for Verifying High-Stakes AI Agreements, Amodo Design (2026). https://amododesign.com/notes/2026-06-23-verification-algorithms/
3. Scaling Recomputation Inference Verification, Amodo Design (2026). https://amododesign.com/notes/2026-09-02-scaling-recomputation-inference-verification/
4. AI 2040 Plan A — Verification SITREP, Amodo Design (2026). https://amododesign.com/ai-verification/plan-a-sitrep/
5. Get Involved in Verification, AI Futures Project (2026). https://ai-2040.com/supplements/verification-plan/get-involved
6. Proof-of-Learning is Currently More Broken Than You Think, C. Fang et al. (2023). https://arxiv.org/abs/2208.03567
7. A System Overview for Near-Term, Low-Trust AI Compute Verification, N. Cankaya (2026). https://intelligence.org/wp-content/uploads/2026/06/A-system-overview-for-near-term-low-trust-AI-compute-verification.pdf
8. Fingerprinting All AI Cluster I/O Without Mutually Trusted Processors, N. Cankaya et al. (2026). https://arxiv.org/abs/2606.10724
9. Bit-Exact AI Inference Verification Without Performance Tradeoffs, N. Cankaya (2026). https://arxiv.org/abs/2606.00279
10. Hawkeye: Reproducing GPU-Level Non-Determinism, E. Badash et al. (2026). https://proceedings.mlsys.org/paper_files/paper/2026/hash/e217c271a57c365a246b0ad39e668ba8-Abstract-Conference.html