# 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-09. Interactive version: https://trustbutveri.fyi/explorer/?mechanisms=M-0015,M-0019&cols=tested

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 development status, security evidence and findings. Definitions: https://trustbutveri.fyi/about/methodology/ (roles, properties and findings) and https://trustbutveri.fyi/about/readiness/ (development status).

## 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 failures: critical / significant / minor. The last three columns are the editors' reading of what the verifier sees. Findings are grouped as known failures, scope limitations and open questions. Only known failures count as failures. Counts are an inventory of published findings, not a risk score.

| Mechanism | Development | Security evidence | Prover | Attack testing | Hardware | Open failures | Weights | Inputs and outputs | Training data |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| Memory wiping and proofs of secure erasure | Proposed | Published security analysis | Adversarial | Analysis | None | 0 / 1 / 0 | not involved | not involved | not involved |
| Chip registries and manufacturing records | Proposed | Published security analysis | Semi-trusted | Analysis | Existing features | 0 / 1 / 0 | not involved | not involved | not involved |

## Claims

No claims chosen.

## Mechanisms

### Memory wiping and proofs of secure erasure

Overwriting a device's memory in a way a verifier can check, so that data from earlier, undeclared work cannot persist in memory the wipe reaches. ([Memory wiping and proofs of secure erasure](https://trustbutveri.fyi/mechanisms/memory-wiping-and-secure-erasure/))

- Assessment: mechanism family.
- Development: Proposed (legacy code R1), assessed for showing that no data from earlier work persists in memory the wipe reaches.
- Security evidence: Published security analysis. Independent evaluation: unassessed. Formal proof: unassessed. Deployment assurance: unassessed.
- Claims in this proposal: none of them.
- Threat model: adversarial prover. Hardware: none. Prover cooperation: required. Attack testing: analysis. Category: Isolation & system architectures.
- What the verifier sees: model weights not involved; inputs and outputs not involved; training data not involved. Overwrites memory with verifier-chosen data; it does not handle model data.

### Chip registries and manufacturing records

Recording each AI chip's identity and owner from the fab onwards, and cryptographically fixing manufacturing records, so that chips can be accounted for later. ([Chip registries and manufacturing records](https://trustbutveri.fyi/mechanisms/chip-registries-and-manufacturing-records/))

- Assessment: mechanism family.
- Development: Proposed (legacy code R1), assessed for a checkable record of which chips were made and who declared owning them.
- Security evidence: Published security analysis. Independent evaluation: unassessed. Formal proof: unassessed. Deployment assurance: unassessed.
- Claims in this proposal: none of them.
- Threat model: semi-trusted prover. Hardware: existing features. Prover cooperation: required. Attack testing: analysis. Category: Compute accounting & provenance.
- What the verifier sees: model weights not involved; inputs and outputs not involved; training data not involved. Records chip identities and owners; it does not handle model data.


## Properties

**Built for an adversarial prover**

- Memory wiping and proofs of secure erasure

**No new hardware needed**

- Memory wiping and proofs of secure erasure
- Chip registries and manufacturing records


## Attack testing

Attack testing records published testing for this use. It does not by itself show independent review, a formal proof or that a deployed system is secure.

**Testing history**

- Memory wiping and proofs of secure erasure: Analysis
- Chip registries and manufacturing records: Analysis


## Limits

**Open significant failures**

- Outside help during challenges (known failure, theoretical argument, in Memory wiping and proofs of secure erasure; https://trustbutveri.fyi/mechanisms/memory-wiping-and-secure-erasure/evidence/flaws/2/) [3][4]. Classic proofs of secure erasure assume the device is isolated during the protocol. Bursuc et al. relax this to a bound on how close a helper can be, enforced by round-trip times. In data centres, remote memory access has round trips of about 1–2 µs, against about 70–200 ns for local DRAM. The MIRI overview therefore says verification depends on ruling out RDMA by latency or physical disconnection.

  Related mechanism: Timed challenge-response and memory-occupation challenges (R2, not in the proposal). Timed challenges bound how far away a helper can be by how quickly it must answer.

  Related mechanism: Bandwidth limits and compartmentalization (R2, not in the proposal). Removing or capping links between groups of accelerators limits remote memory access during a challenge.
- Documents and serial numbers can be forged (known failure, theoretical argument, in Chip registries and manufacturing records; https://trustbutveri.fyi/mechanisms/chip-registries-and-manufacturing-records/evidence/flaws/2/) [10]. Avellar and Grunewald note that export documents can be forged, that companies can hide information behind obscure corporate structures, and that it may be possible to forge serial numbers on chips and racks. They recommend cryptographic attestation of a powered-on chip as an extra check.

**Scope limitations**

- Memory the wipe cannot reach (scope limitation, open question, in Memory wiping and proofs of secure erasure; https://trustbutveri.fyi/mechanisms/memory-wiping-and-secure-erasure/evidence/flaws/1/) [5][6]. Amodo's inventory of a GB200 system lists many memory stores beyond GPU HBM and host DRAM. It notes that SSD controller DRAM sits on a private bus that host commands cannot read or write, and that its optimized algorithm leaves 25 GiB of HBM unattested. It also asks how switch memory could be wiped.
- Gap between erased and total memory (scope limitation, theoretical argument, in Memory wiping and proofs of secure erasure; https://trustbutveri.fyi/mechanisms/memory-wiping-and-secure-erasure/evidence/flaws/3/) [3]. Bursuc et al. note that memory left between the erased region and the device's full memory could hold data, and that their bounds are tighter only against a restricted adversary.
- Records cover only chips that were recorded (scope limitation, theoretical argument, in Chip registries and manufacturing records; https://trustbutveri.fyi/mechanisms/chip-registries-and-manufacturing-records/evidence/flaws/1/) [11][13]. A registry or commitment accounts only for chips entered into it. Cankaya asks how a verifier would know it had found all chips, or how much "dark compute" remains, and notes that a fraudulent original record would mean unregistered chips had been made in advance. Halstead and Larsen propose reconstructing earlier production by auditing upstream suppliers.

  Related mechanism: Remote detection of data centres (R1, not in the proposal). Looks for large data centres that were never declared, which a registry cannot show.
- Insiders could alter records before they are fixed (scope limitation, theoretical argument, in Chip registries and manufacturing records; https://trustbutveri.fyi/mechanisms/chip-registries-and-manufacturing-records/evidence/flaws/3/) [11]. Cankaya argues that insiders who can photograph process secrets could also tamper with production records. A commitment makes changes after publication detectable, but it cannot show that the records were accurate when committed.

**Not yet demonstrated**

- Memory wiping and proofs of secure erasure: Proposed (legacy code R1), assessed for showing that no data from earlier work persists in memory the wipe reaches
- Chip registries and manufacturing records: Proposed (legacy code R1), assessed for a checkable record of which chips were made and who declared owning them


## Possible additions

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

- **Bandwidth limits and compartmentalization** (Research demonstration (legacy code R2), assessed for monitoring inter-node traffic with operator-run software on four GPUs)
  - Bears on the open significant failure "Outside help during challenges" in Memory wiping and proofs of secure erasure. Removing or capping links between groups of accelerators limits remote memory access during a challenge.
- **Timed challenge-response and memory-occupation challenges** (Research demonstration (legacy code R2), assessed for detecting whether a GPU is doing other work)
  - Bears on the open significant failure "Outside help during challenges" in Memory wiping and proofs of secure erasure. Timed challenges bound how far away a helper can be by how quickly it must answer.
  - Memory wiping and proofs of secure erasure waits on it: Timed challenges must exclude remote memory and other helpers.


## Dependencies

**Missing prerequisites**

- Timed challenge-response and memory-occupation challenges (Research demonstration (legacy code R2), assessed for detecting whether a GPU is doing other work), needed by Memory wiping and proofs of secure erasure

**Blockers**

- Memory wiping and proofs of secure erasure: Wipes take time: tens of minutes for a pod's volatile memory and hours for SSDs, displacing work. (performance & compatibility) [4][5][6]
- Memory wiping and proofs of secure erasure: Timed challenges must exclude remote memory and other helpers. (coverage & hidden compute; waits on Timed challenge-response and memory-occupation challenges) [3][4]
- Memory wiping and proofs of secure erasure: All memory stores in a system must be inventoried and wiped at the same time. (coverage & hidden compute) [5]
- Chip registries and manufacturing records: No implementation of an AI chip registry has been publicly reported, and covering re-exports would need cooperation from re-exporters and foreign governments that may not be feasible everywhere. (access & governance) [9][10]
- Chip registries and manufacturing records: Linking records to physical chips needs hard-to-spoof unique IDs and inspections. (hardware trust) [9][10][11]
- Chip registries and manufacturing records: Chips produced before a registry starts must be reconstructed from supplier records. (coverage & hidden compute) [11][13]


## What the verifier sees

- Model weights: shown by none; depends on the design for none; hidden by none; not involved in Memory wiping and proofs of secure erasure and Chip registries and manufacturing records; unspecified for none.
- Inputs and outputs: shown by none; depends on the design for none; hidden by none; not involved in Memory wiping and proofs of secure erasure and Chip registries and manufacturing records; unspecified for none.
- Training data: shown by none; depends on the design for none; hidden by none; not involved in Memory wiping and proofs of secure erasure and Chip registries and manufacturing records; unspecified for none.

## Implementations

- Memory wiping and proofs of secure erasure: [AI 2040 inference-only verification stack](https://trustbutveri.fyi/implementations/ai-2040-inference-only-verification-plan/) (R1, proposed architecture); [Low-trust AI compute verification system overview](https://trustbutveri.fyi/implementations/low-trust-compute-verification-system-overview/) (R1, proposed architecture)
- Chip registries and manufacturing records: none on the map

## Sources

1. Verification Plan, R. Dean (2026). https://ai-2040.com/supplements/verification-plan
2. Secure Code Update for Embedded Devices via Proofs of Secure Erasure, D. Perito & G. Tsudik (2010). https://link.springer.com/chapter/10.1007/978-3-642-15497-3_39
3. Software-Based Memory Erasure with Relaxed Isolation Requirements, S. Bursuc et al. (2024). https://ieeexplore.ieee.org/document/10664348/
4. 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
5. Memory Wipes - Performance Analysis, Amodo Design (2026). https://amododesign.com/notes/2026-07-01-memory-wiping/
6. Improving Disk Wiping Speed for Memory Wipes, Amodo Design (2026). https://amododesign.com/notes/2026-09-14-disk-wiping-speed/
7. Amodo-Design/PoSE-Memory-Wiping (GitHub repository), Amodo Design (2026). https://github.com/Amodo-Design/PoSE-Memory-Wiping
8. Empirical Evaluation of Memory-Erasure Protocols, R. Gil-Pons et al. (2025). https://www.scitepress.org/Papers/2025/135548/135548.pdf
9. Verifying International Agreements on AI: Six Layers of Verification for Rules on Large-Scale AI Development and Deployment, M. Baker et al. (2025). https://www.rand.org/pubs/working_papers/WRA4077-1.html
10. Near-Term Verification Methods for AI Chip Exports, B. Avellar & E. Grunewald (2026). https://www.iaps.ai/research/near-term-verification-methods-for-ai-chip-exports
11. TSMC most definitely has a golden record of all AI chips it made, N. Cankaya (2025). https://nacicankaya.substack.com/p/tsmc-most-definitely-has-a-golden
12. Hardware-Level Governance of AI Compute: A Feasibility Taxonomy for Regulatory Compliance and Treaty Verification, S. Ansari (2026). https://arxiv.org/abs/2604.04712
13. Covert AI Projects, B. Halstead & T. Larsen (2026). https://ai-2040.com/supplements/covert-ai-projects