verifiable.pro

Resources

Papers, specifications, tools and reports that help someone check a claim about an AI system, with trusted execution environments first. A listing is not an endorsement. The “Link checked” date says when we last opened the link.

Reading paths

Start with TEEs

First learn the vocabulary of remote attestation, in which a machine signs a record of the software it loaded so that others can check it. Then read about the CPU and GPU platforms that attested AI services run on.

  1. RFC 9334: Remote ATtestation procedureS (RATS) ArchitectureDefines the attester, verifier and relying party that every later document assumes.
  2. Intel TDX Demystified: A Top-Down ApproachHow TDX is designed to isolate whole virtual machines, explained by researchers outside Intel.
  3. AMD SEV-SNP: Strengthening VM Isolation with Integrity Protection and MoreWhat SEV-SNP adds against a malicious hypervisor (the software that manages virtual machines), and what AMD leaves out of scope.
  4. Arm Confidential Compute ArchitectureHow Arm's Realms are designed to separate a workload from the hypervisor that still schedules it.
  5. Confidential Computing on NVIDIA H100 GPUs for Secure and Trustworthy AIHow a GPU joins the trust boundary, and which GPU memory NVIDIA does not encrypt.
  6. Private Cloud Compute Security GuideA complete service design, with a research environment that lets outsiders run and inspect the node software.

Where TEE protection ends

Published attacks show where isolation and attestation break down. Most of them need physical access to the server.

  1. TEE.fail: Breaking Trusted Execution Environments via DDR5 Memory Bus InterpositionA physical attack that extracts keys to forge TDX attestation reports (quotes), and shows that GPU reports can be borrowed from other machines.
  2. BadRAM: Practical Memory Aliasing Attacks on Trusted Execution EnvironmentsResearchers altered a memory module with under $10 of equipment and replayed a genuine measurement for a backdoored SEV-SNP VM.
  3. Battering RAM: Low-Cost Interposer Attacks on Confidential Computing via Dynamic Memory AliasingAn interposer, placed between the processor and memory, passes boot checks and later breaks SEV-SNP attestation on fully patched systems.
  4. Proof of Cloud: Data Center Execution Assurance for Confidential VMsA proposed response: binding attestation to a machine in a trusted data center.
  5. Machine Learning with Confidential Computing: A Systematization of KnowledgeA survey of what TEEs do and do not give machine-learning workloads.

Private AI services, as their providers describe them

Providers describe their own designs here, so read each as the provider's claim and note what it lets outsiders check.

  1. Private Cloud Compute: A new frontier for AI privacy in the cloudApple's requirements for cloud AI that users' devices can verify.
  2. Building Private Processing for AI tools on WhatsAppMeta's design for WhatsApp, which Trail of Bits audited before launch.
  3. Private AI Compute: our next step in building private and helpful AIGoogle's platform, where most attestation checks run inside Google.
  4. Confidential Inference via Trusted Virtual MachinesAn early design in which only a small attested loader can decrypt prompts and weights.
  5. Azure AI Confidential Inferencing: Technical Deep-DiveMicrosoft's planned design, in which a key service releases decryption keys only to attested GPU VMs.
  6. RFC 9458: Oblivious HTTPThe relay protocol several services use to hide a client's network address from the server.

Other ways to check, compared with TEEs

Signatures, audits, re-execution and proofs each ask you to trust different parties than a TEE does. Start with one or two readings on each.

  1. SigstoreSignatures and a public log: what a signer vouches for.
  2. Black-Box Access is Insufficient for Rigorous AI AuditsAudits: why the depth of access decides what an audit can find.
  3. TOPLOC: A Locality Sensitive Hashing Scheme for Trustless Verifiable InferenceRe-execution: fingerprints of a model's intermediate values (activations) that tolerate differences across GPU types.
  4. Verde: Verification via Refereed Delegation for Machine Learning ProgramsRe-execution with a referee that narrows a dispute between providers to a single operation.
  5. zkLLM: Zero Knowledge Proofs for Large Language ModelsProofs: a zero-knowledge proof system, which lets others check that a model computed an output correctly without seeing its weights. The authors applied it to a 13-billion-parameter model.
  6. A Survey of Zero-Knowledge Proof Based Verifiable Machine LearningProofs: where zero-knowledge machine learning stands and what limits it.

Showing 170 of 170

Confidential computing & attestation 27

You trust: the chip vendor and the measured software

Architecture and standards 5

  • RFC 9334: Remote ATtestation procedureS (RATS) Architecture

    IETF · 2023 · Specification Link checked 20 Oct 2026

    Summary

    Informational IETF RFC that defines the roles and messages of remote attestation. The roles include attesters, verifiers and relying parties; the messages include evidence, endorsements, reference values and attestation results.

  • Confidential Computing Consortium

    Linux Foundation · 2019 · Organization Link checked 20 Oct 2026

    Summary

    Linux Foundation community that works to speed up the adoption of trusted execution environment (TEE) technologies. It maintains open-source projects and attestation specifications for them.

  • RFC 9458: Oblivious HTTP

    IETF · 2024 · Standard Link checked 20 Oct 2026

    Summary

    IETF standards-track protocol in which a relay forwards encrypted HTTP requests. The server never sees the client's IP address, and the relay never sees the content. Apple and Meta route AI requests through third-party OHTTP relays to hinder attacks that target specific users.

  • Caliptra

    CHIPS Alliance (Linux Foundation) · 2022 · Project Link checked 20 Oct 2026

    Summary

    Root-of-trust block that chip makers integrate into datacenter CPUs, GPUs and other systems on chip. It provides device identity, measured boot and attestation. Its specification, hardware design (RTL), ROM and firmware are open source. AMD, Google, Microsoft and NVIDIA announced it at the Open Compute Project summit in 2022.

  • RFC 9711: The Entity Attestation Token (EAT)

    IETF · 2025 · Standard Link checked 20 Oct 2026

    Summary

    IETF standards-track format for attestation evidence and attestation results, carried as a CBOR Web Token (CWT) or JSON Web Token (JWT). It defines common claims such as a nonce that shows the evidence is fresh, a universal entity ID (UEID), the hardware manufacturer, and the software name and version. It follows the RATS architecture of RFC 9334.

CPU TEEs 3

  • AMD SEV-SNP: Strengthening VM Isolation with Integrity Protection and More

    AMD · 2020 · Report Link checked 20 Oct 2026

    Summary

    AMD white paper describing SEV-SNP. SEV-SNP adds memory integrity protection against a malicious hypervisor to encrypted virtual machines. It signs attestation reports with a key unique to each chip and its TCB version, the versions of the chip's trusted components.

  • Intel TDX Demystified: A Top-Down Approach

    Pau-Chen Cheng et al. · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Analysis of Intel Trust Domain Extensions (TDX) by researchers outside Intel. It explains how TDX is designed to isolate virtual machines with encrypted, integrity-protected memory, and how its remote attestation works.

  • Arm Confidential Compute Architecture

    Arm · 2021 · Specification Link checked 20 Oct 2026

    Summary

    Armv9-A security architecture in which the Realm Management Extension (RME) creates hardware-isolated execution environments called Realms. The open-source Realm Management Monitor (RMM) manages them. The host hypervisor still decides which Realms run and what memory they receive. But the architecture is designed so that the hypervisor cannot access or modify the Realms' code and data.

GPU confidential computing 2

  • Confidential Computing on NVIDIA H100 GPUs for Secure and Trustworthy AI

    NVIDIA · 2023 · Report Link checked 20 Oct 2026

    Summary

    NVIDIA's technical overview of confidential computing on H100 GPUs. It covers the on-die root of trust, measured boot, signed attestation reports and encrypted transfers between CPU and GPU. It notes that the on-package high-bandwidth memory (HBM) is not encrypted.

  • NVIDIA Attestation

    NVIDIA · Tool Link checked 20 Oct 2026

    Summary

    Documentation for NVIDIA's attestation services and for the SDKs that verify GPU evidence. The services include the Remote Attestation Service (NRAS) and the Reference Integrity Manifest (RIM) service, which supplies reference values. They also include an OCSP service, which reports whether certificates have been revoked.

AI services that use attestation 6

  • Private Cloud Compute: A new frontier for AI privacy in the cloud

    Apple · 2024 · Project Link checked 20 Oct 2026

    Summary

    Apple's design for processing Apple Intelligence requests in the cloud. It is built around five requirements: stateless computation, enforceable guarantees, no privileged runtime access, non-targetability and verifiable transparency.

  • Private Cloud Compute Security Guide

    Apple · 2024 · Report Link checked 20 Oct 2026

    Summary

    Apple's technical documentation of the Private Cloud Compute (PCC) design. The accompanying Virtual Research Environment (VRE) runs PCC node software on a Mac. Apple also provides source code for selected security-critical components.

  • Building Private Processing for AI tools on WhatsApp

    Meta · 2025 · Project Link checked 20 Oct 2026

    Summary

    Meta's design for running WhatsApp AI features in confidential virtual machines with confidential-computing GPUs. Clients check attestations against a third-party log over RA-TLS, which binds remote attestation to a TLS connection. They connect through Oblivious HTTP (OHTTP) relays, which hide a client's IP address from the server.

  • Private AI Compute: our next step in building private and helpful AI

    Google · 2025 · Project Link checked 20 Oct 2026

    Summary

    Google's announcement of a platform that runs Gemini models on its Tensor Processing Units (TPUs) with Titanium Intelligence Enclaves. User devices connect to the platform through remote attestation and encryption.

  • Confidential Inference via Trusted Virtual Machines

    Anthropic, with Pattern Labs · 2025 · Report Link checked 20 Oct 2026

    Summary

    Anthropic's early-stage design for its inference server. Only a small attested loader, rather than the whole server, can decrypt prompts and model weights. Boot measurements recorded by a Trusted Platform Module (TPM) control the release of keys.

  • Azure AI Confidential Inferencing: Technical Deep-Dive

    Mark Russinovich (Microsoft) · 2024 · Report Link checked 20 Oct 2026

    Summary

    Microsoft's planned design for confidential inferencing in Azure OpenAI Service, announced as an upcoming preview. Clients encrypt prompts with Oblivious HTTP (OHTTP). A key management service releases the decryption keys only to attested confidential GPU VMs built on AMD SEV-SNP and NVIDIA H100. A transparency ledger records the deployed code, container policies and key release policies.

Attacks and limits 4

  • TEE.fail: Breaking Trusted Execution Environments via DDR5 Memory Bus Interposition

    Jalen Chuang et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Physical attack that extracts cryptographic keys from Intel TDX and AMD SEV-SNP machines with an interposer, a device attached to the DDR5 memory bus. The keys include an Intel attestation key used to forge TDX quotes, Intel's name for attestation reports. The work also shows that NVIDIA GPU attestations can be borrowed from other machines, because they are not bound to a specific confidential VM.

  • Proof of Cloud: Data Center Execution Assurance for Confidential VMs

    Filip Rezabek et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Design that binds confidential-VM attestation to evidence from the host's Trusted Platform Module (TPM). A verifier then learns that the workload runs on a machine in a trusted data center. The binding is also designed to block relay attacks, which pass off attestation from another machine.

  • BadRAM: Practical Memory Aliasing Attacks on Trusted Execution Environments

    Jesse De Meulemeester et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Attack in which a memory module misreports its size because its serial presence detect (SPD) chip has been altered. The false size creates address aliases, two addresses that point to the same memory location. With under $10 of equipment, an attacker can use them to bypass AMD SEV-SNP memory protections. The attacker can also replay a genuine attestation measurement for a backdoored VM. AMD responded with firmware that checks memory configuration at boot; Intel TDX and Scalable SGX already had this defense.

  • Battering RAM: Low-Cost Interposer Attacks on Confidential Computing via Dynamic Memory Aliasing

    Jesse De Meulemeester et al. · 2026 · Paper Link checked 20 Oct 2026

    Summary

    Attack with an interposer costing under $50, placed between the processor and DDR4 memory. The interposer behaves normally during boot-time checks and later, at runtime, creates address aliases. This gives plaintext access to Intel Scalable SGX enclave memory and breaks AMD SEV-SNP attestation on fully patched systems. Intel and AMD said physical attacks on DRAM are out of scope for their current products.

Performance 1

  • Benchmarking Confidential Computing Performance on NVIDIA Blackwell GPUs

    Amean Asad, Ansgar Grunseid · 2026 · Paper Link checked 20 Oct 2026

    Summary

    Paired measurements of LLM inference and training on B200 GPUs in Intel TDX confidential VMs. With a correctly configured stack, the authors report about 1 to 3 percent inference throughput overhead. With stock settings, they report 30 to 40 percent.

TEEs in evaluations, agents and model security 6

Model & data supply chain 24

You trust: the signer and its keys

  • SLSA Specification v1.2

    SLSA project · 2025 · Specification Link checked 20 Oct 2026

    Summary

    Framework of incremental supply-chain security levels, organized into Build and Source tracks. It recommends formats for signed statements about artifacts (attestations), including build provenance, which records how an artifact was built.

  • Sigstore

    OpenSSF (Linux Foundation) · 2021 · Project Link checked 20 Oct 2026

    Summary

    Open-source project for signing and verifying software artifacts with short-lived certificates tied to an identity. Signing events are recorded in the Rekor transparency log, a public append-only log that anyone can check.

  • Model Transparency

    Sigstore · 2023 · Tool Link checked 20 Oct 2026

    Summary

    Reference library and command-line tool (model_signing) for signing ML models with Sigstore, public keys or certificates. It verifies a model against a signed manifest of its file hashes. Version 1.0 was released in April 2025.

  • OpenSSF Model Signing (OMS) Specification

    OpenSSF AI/ML Working Group · 2025 · Specification Link checked 20 Oct 2026

    Summary

    Format for a detached model signature, which is stored apart from the files it signs. The format does not depend on any one implementation. One signature covers the model's artifacts, such as weights, configuration files and tokenizers. It can use bare keys, certificate chains or Sigstore.

  • in-toto Attestation Framework

    in-toto project · 2021 · Specification Link checked 20 Oct 2026

    Summary

    Specification for verifiable claims about how software was produced. It defines a standard statement format and vetted predicate types, which name the kind of claim being made. Sigstore's model signatures carry in-toto statements.

  • Reproducible Builds

    Reproducible Builds project · Project Link checked 20 Oct 2026

    Summary

    Project that defines and promotes reproducible builds. In a reproducible build, any party can recreate bit-for-bit identical artifacts from the same source, environment and instructions. This lets anyone check a binary against its source code.

  • RFC 9943: An Architecture for Trustworthy and Transparent Digital Supply Chains

    IETF · 2026 · Standard Link checked 20 Oct 2026

    Summary

    IETF architecture for Supply Chain Integrity, Transparency and Trust (SCITT), published as a Proposed Standard. Issuers register signed statements about artifacts with a transparency service. The service records them in an append-only ledger and returns receipts showing that each statement was recorded.

  • Machine Learning Bill of Materials (AI/ML-BOM)

    OWASP CycloneDX · 2023 · Specification Link checked 20 Oct 2026

    Summary

    CycloneDX capability for describing models, datasets and their dependencies in a machine-readable bill of materials, including dataset provenance and training methods. AI support arrived in CycloneDX 1.5. CycloneDX 1.6 was published as Ecma standard ECMA-424.

  • SPDX Specification 3.0.1: AI Profile

    SPDX (Linux Foundation) · 2024 · Specification Link checked 20 Oct 2026

    Summary

    SPDX profile for documenting AI software packages, with fields such as autonomy type, energy consumption, safety risk assessment, training information and limitations.

  • Model Cards for Model Reporting

    Margaret Mitchell et al. · 2018 · Paper Link checked 20 Oct 2026

    Summary

    Proposes model cards: short documents that accompany trained models and report their intended uses and evaluation results across relevant conditions and groups.

  • The Data Provenance Initiative: A Large Scale Audit of Dataset Licensing & Attribution in AI

    Shayne Longpre et al. · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Audit that traces the sources, creators and licenses of more than 1,800 text datasets. On widely used hosting sites, it finds license information omitted in over 70 percent of cases.

  • Croissant: A Metadata Format for ML-Ready Datasets

    Mubashara Akhtar et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Metadata format that gives ML datasets a shared, machine-readable description across tools, frameworks and repositories. MLCommons hosts its specification and code.

  • Poisoning Web-Scale Training Datasets is Practical

    Nicholas Carlini et al. · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Shows two practical poisoning attacks on web-scale datasets, in which attackers plant bad data in a training set. One of them could have poisoned 0.01 percent of LAION-400M for about 60 US dollars. The paper also recommends low-overhead defenses.

  • Atlas: A Framework for ML Lifecycle Provenance & Transparency

    Marcin Spoczynski, Marcela S. Melara, Sebastian Szyller · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Framework for attestable ML pipelines. It combines trusted hardware, transparency logs and open provenance specifications to record a model's lineage (the data and steps behind it) from training through deployment.

  • Signing ML Artifacts: Building towards tamper-proof ML metadata records

    Coalition for Secure AI (OASIS) · 2025 · Report Link checked 20 Oct 2026

    Summary

    Coalition for Secure AI paper on model-signing roles, components and maturity levels. It includes NVIDIA's account of shipping an OpenSSF Model Signing (OMS) signature with every NVIDIA model published in its NGC catalog since March 2025.

  • Independence Tests for Language Models

    Sally Zhu et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Statistical tests of whether two language models, given their weights, were trained from independent random initializations (starting weights). One test, on matched hidden activations, resists adversarial changes and can locate components derived from another model. For example, it shows how Llama 3.1-8B was pruned to initialize Llama 3.2-3B.

    Model & data supply chainVerifiable inference & computation

  • Model Provenance Testing for Large Language Models

    Ivica Nikolic, Teodora Baluta, Prateek Saxena · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Black-box framework that decides whether one LLM was derived from another by applying multiple hypothesis testing to their outputs. On benchmarks of more than 600 models, it reports 90–95% precision and 80–90% recall.

  • RFC 6962: Certificate Transparency

    IETF · 2013 · Specification Link checked 20 Oct 2026

    Summary

    Experimental IETF protocol, now obsoleted by RFC 9162 (version 2.0). Public append-only logs built on Merkle trees (hash trees) record TLS certificates, so anyone can audit certificate authorities. Anyone can also check the logs: Merkle audit paths show that a certificate is included, and consistency proofs show that a log has only been appended to.

    Model & data supply chainAgent identity & accountability

  • Datasheets for Datasets

    Timnit Gebru et al. · 2018 · Paper Link checked 20 Oct 2026

    Summary

    Proposes that every dataset be accompanied by a datasheet documenting its motivation, composition, collection process and recommended uses, by analogy with datasheets for electronic components.

  • Planting Undetectable Backdoors in Machine Learning Models

    Shafi Goldwasser et al. · 2022 · Paper Link checked 20 Oct 2026

    Summary

    Shows that a service provider entrusted with training can plant a backdoor that no observer with limited computing power can detect. In one construction, the backdoor stays undetectable even to someone given the full network and its training data.

  • Sleeper Agents: Training Deceptive LLMs that Persist Through Safety Training

    Evan Hubinger et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Trains proof-of-concept LLMs with backdoors, such as writing exploitable code when the prompt states that the year is 2024. The paper finds that supervised fine-tuning, reinforcement learning and adversarial training can fail to remove them. Adversarial training sometimes teaches the models to hide the behavior.

  • Poisoning Attacks on LLMs Require a Near-constant Number of Poison Samples

    Alexandra Souly et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Pretraining experiments on models from 600M to 13B parameters, in which 250 poisoned documents implanted a backdoor at every scale. This indicates that the number of poison samples an attack needs stays near-constant as models and datasets grow.

  • Explanatory Notice and Template for the Public Summary of Training Content for general-purpose AI models

    European Commission · 2025 · Standard Link checked 20 Oct 2026

    Summary

    Mandatory template under Article 53(1)(d) of the EU AI Act for the public summary of training content. Providers of general-purpose AI models must publish this summary. It covers data sources such as large public datasets, the most-scraped web domains and user data.

    Model & data supply chainGovernance & compute verification

  • AI Cyber Security Code of Practice

    UK Department for Science, Innovation and Technology · 2025 · Standard Link checked 20 Oct 2026

    Summary

    Voluntary UK code that sets 13 baseline security principles for AI systems across five lifecycle phases. The principles include securing the supply chain; documenting data, models and prompts; and re-running evaluations on released models before use.

Content provenance & watermarking 22

You trust: the signer and its keys

  • Content Credentials: C2PA Technical Specification (version 2.4)

    C2PA · 2026 · Specification Link checked 20 Oct 2026

    Summary

    Defines C2PA manifests: signed assertions about a media asset's origin and edits. Cryptographic hashes bind a manifest to the content, and fingerprints or invisible watermarks can optionally bind it too.

  • Content Authenticity Initiative

    Content Authenticity Initiative · 2019 · Organization Link checked 20 Oct 2026

    Summary

    Community founded by Adobe in 2019 that promotes adoption of C2PA Content Credentials and develops open-source tools for them.

  • Reducing Risks Posed by Synthetic Content: An Overview of Technical Approaches to Digital Content Transparency

    NIST · 2024 · Report Link checked 20 Oct 2026

    Summary

    NIST report (AI 100-4) that surveys technical approaches to digital content transparency and their limitations. The approaches include tracking provenance through watermarks and metadata, and detecting synthetic content.

  • A Watermark for Large Language Models

    John Kirchenbauer et al. · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Text watermark that softly favors a pseudorandom set of 'green' tokens at each generation step. A statistical test can detect it without access to the model.

  • Scalable watermarking for identifying large language model outputs

    Sumanth Dathathri et al. (Google DeepMind) · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Describes SynthID-Text, a sampling-based text watermark that works with speculative sampling, a technique for faster generation. It also reports a live experiment that assessed nearly 20 million Gemini responses for quality.

  • Google SynthID

    Google DeepMind · 2023 · Tool Link checked 20 Oct 2026

    Summary

    Google DeepMind's watermarking for AI-generated images, audio, text and video. Its SynthID Detector portal checks content from Google and from partners including OpenAI, NVIDIA and Kakao.

  • The Stable Signature: Rooting Watermarks in Latent Diffusion Models

    Pierre Fernandez et al. · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Fine-tunes a latent diffusion model's decoder so that every generated image carries an invisible watermark that remains detectable after edits such as cropping.

  • Undetectable Watermarks for Language Models

    Miranda Christ, Sam Gunn, Or Zamir · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Cryptographic watermark for language models whose outputs cannot be distinguished from the original model's outputs without the secret key.

  • Watermarks in the Sand: Impossibility of Strong Watermarking for Generative Models

    Hanlin Zhang et al. · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Proves that strong watermarking of generative model outputs is impossible under stated assumptions. A strong watermark is one that cannot be removed without noticeably degrading output quality. The paper also gives a generic removal attack that worked against three text watermarking schemes.

  • Code of Practice on Transparency of AI-generated Content

    European Commission · 2026 · Standard Link checked 20 Oct 2026

    Summary

    Voluntary code that helps providers and deployers of generative AI meet the marking and labeling obligations in Article 50 of the EU AI Act. These obligations apply from 2 August 2026. The final version of the code was published on 10 June 2026.

  • Apple Reference Image: A New Approach for Verified Photography

    Apple · 2026 · Project Link checked 20 Oct 2026

    Summary

    Opt-in iPhone camera mode in which the image sensor signs pixel data at capture. The Secure Enclave, the iPhone's security processor, signs other metadata. Private Cloud Compute then develops the images. Apple contrasts the mode with C2PA-based approaches.

  • How to Hack Time, With C2PA

    David Buchanan · 2026 · Report Link checked 20 Oct 2026

    Summary

    Security write-up on C2PA's exclusion ranges, the parts of a file that a signer may leave out of the signed hash. The author shows that a signer can exclude the whole file. The claim signature and trusted timestamp then cover none of its content, so later edits do not invalidate them.

  • 人工智能生成合成内容标识办法 (Measures for Labeling AI-Generated Synthetic Content)

    Cyberspace Administration of China et al. · 2025 · Standard Link checked 20 Oct 2026

    Summary

    Chinese rules issued by the Cyberspace Administration of China and three other agencies, in force since 1 September 2025. Providers must add explicit labels, which users can see or hear, to AI-generated content. They must also write implicit labels into its metadata. Distribution platforms must check the metadata and label the content accordingly.

  • Framework Act on the Development of Artificial Intelligence and the Creation of a Foundation for Trust

    Republic of Korea · 2025 · Standard Link checked 20 Oct 2026

    Summary

    South Korean law in force since 22 January 2026. The link is to the Korea Legislation Research Institute's unofficial English translation. The law requires generative AI outputs to be labeled. AI-generated sounds, images or videos that are hard to tell apart from real ones must be clearly disclosed. The law also sets risk-management duties for AI systems trained above a compute threshold.

    Content provenance & watermarkingGovernance & compute verification

  • JPEG Trust (ISO/IEC 21617)

    ISO/IEC JPEG Committee · 2025 · Standard Link checked 20 Oct 2026

    Summary

    Multi-part ISO/IEC standard from the JPEG committee for annotating media assets with information on provenance, authenticity, attribution, rights and integrity. Part 1, Core foundation, was published as ISO/IEC 21617-1:2025 in January 2025. Parts on trust profiles, watermarking and reference software are in development.

  • C2PA Conformance Program

    C2PA · 2025 · Project Link checked 20 Oct 2026

    Summary

    C2PA program, launched in mid-2025, that covers generator products, validator products and certification authorities. It holds them to the Content Credentials specification, certificate policy and security requirements. It publishes the Conforming Products List, the C2PA Trust List and a TSA Trust List for time-stamping authorities.

  • How Pixel and Android are bringing a new level of trust to your images with C2PA Content Credentials

    Google · 2025 · Project Link checked 20 Oct 2026

    Summary

    Google's account of Content Credentials in the Pixel 10 camera and Google Photos. Google says the camera app reached Assurance Level 2 of the C2PA Conformance Program through hardware-backed key attestation. It also says the app signs each image with a single-use certificate and timestamps offline captures with an on-device time-stamping authority.

  • SoK: Watermarking for AI-Generated Content

    Xuandong Zhao et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Structured survey, or systematization of knowledge (SoK), on watermarking for AI-generated content. It formalizes the definitions and desired properties of watermarking schemes and examines their objectives and threat models. It also reviews evaluation strategies and representative schemes, and discusses regulatory context and open challenges.

  • WAVES: Benchmarking the Robustness of Image Watermarks

    Bang An et al. · 2024 · Benchmark Link checked 20 Oct 2026

    Summary

    Benchmark for image watermark robustness that combines detection and identification tasks with a standardized set of stress tests. The tests range from common image distortions to diffusion-based and adversarial attacks. After each attack, it measures both the loss of image quality and how well the watermark is still detected.

  • MarkLLM: An Open-Source Toolkit for LLM Watermarking

    Tsinghua University (THU-BPM) · 2024 · Tool Link checked 20 Oct 2026

    Summary

    Open-source toolkit that implements many LLM text watermarking algorithms, including KGW, Unigram and SynthID-Text, behind one interface. It visualizes how they work and provides tools to evaluate detectability, robustness and text quality.

  • Video Seal: Open and Efficient Video Watermarking

    Pierre Fernandez et al. (Meta) · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Open-source neural video watermarking method from Meta. It jointly trains an embedder and an extractor, applying transformations such as video compression between them. It propagates watermarks across frames, so not every high-resolution frame has to be watermarked.

  • PAI’s Responsible Practices for Synthetic Media

    Partnership on AI · 2023 · Report Link checked 20 Oct 2026

    Summary

    Partnership on AI framework, launched in February 2023, that recommends consent, disclosure and transparency practices for builders, creators and distributors of synthetic media. PAI collects case studies from supporters but does not audit or certify them.

Agent identity & accountability 16

You trust: the signer and its keys

  • Infrastructure for AI Agents

    Alan Chan et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Defines agent infrastructure as systems and protocols outside agents. It has three functions: attributing actions to agents and their users, shaping agents' interactions, and detecting and remedying harmful actions.

  • Visibility into AI Agents

    Alan Chan et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Assesses agent identifiers, real-time monitoring and activity logging as ways to learn where, why, how and by whom AI agents are used.

  • IDs for AI Systems

    Alan Chan et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Proposes IDs attached to instances of AI systems so that users and investigators can find associated information such as certifications and responsible parties.

  • Authenticated Delegation and Authorized AI Agents

    Tobin South et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Extends OAuth 2.0 and OpenID Connect, standards for authorization and sign-in, with agent-specific credentials and metadata. Users can then give AI agents authority that is limited in scope and can be audited.

  • Identity Management for Agentic AI

    OpenID Foundation · 2025 · Report Link checked 20 Oct 2026

    Summary

    OpenID Foundation whitepaper on applying OAuth 2.1, enterprise single sign-on and SCIM (a standard for managing user accounts) to AI agents. It also covers open problems such as delegated authority, recursive delegation (agents delegating to other agents) and the number of consent requests users face.

  • Accelerating the Adoption of Software and Artificial Intelligence Agent Identity and Authorization

    NIST NCCoE · 2026 · Report Link checked 20 Oct 2026

    Summary

    Concept paper from NIST's National Cybersecurity Center of Excellence (NCCoE) on applying identity and authorization standards to AI agents. It sought input on identification, authorization, auditing, non-repudiation and prompt-injection controls.

  • Verifiable Credentials Data Model v2.0

    W3C · 2025 · Standard Link checked 20 Oct 2026

    Summary

    W3C Recommendation that defines a data model for tamper-evident credentials whose authorship can be verified cryptographically. Issuers, holders and verifiers exchange these credentials.

  • Agent2Agent (A2A) Protocol Specification

    A2A Project (Linux Foundation) · 2026 · Specification Link checked 20 Oct 2026

    Summary

    Specification for communication between AI agents. Version 1.0, released in March 2026, defines how providers can sign the Agent Cards that describe their agents. They sign with JSON Web Signatures, so clients can check a card's origin and integrity.

  • Agent Payments Protocol (AP2)

    Google; FIDO Alliance · 2025 · Specification Link checked 20 Oct 2026

    Summary

    Open protocol for payments initiated by AI agents. Signed mandates record what the user authorized and form an audit trail. Google donated it to the FIDO Alliance in April 2026.

  • HTTP Message Signatures for automated traffic

    IETF Web Bot Auth Working Group · 2026 · Specification Link checked 20 Oct 2026

    Summary

    IETF working-group Internet-Draft, not yet an RFC, that lets bots and agents sign HTTP requests so servers can verify their identity. A Signature-Agent header tells servers where to find the signing keys.

  • Efficient Data Structures for Tamper-Evident Logging

    Scott A. Crosby, Dan S. Wallach · 2009 · Paper Link checked 20 Oct 2026

    Summary

    Tree-based tamper-evident log, which makes any later deletion or change detectable. An untrusted logger can prove that events are still present and that the log is consistent with earlier versions. The proofs stay small, growing only logarithmically with the log's size.

    Agent identity & accountabilityModel & data supply chain

  • Workload Identity in Multi System Environments (WIMSE)

    IETF · 2024 · Project Link checked 20 Oct 2026

    Summary

    IETF working group, chartered in March 2024, that standardizes identity and authentication for software workloads across trust domains. It builds on OAuth, JWT and SPIFFE. Its drafts cover workload tokens, workload-to-workload authentication and an AI identity management system.

  • OpenTelemetry GenAI Semantic Conventions

    OpenTelemetry · 2024 · Specification Link checked 20 Oct 2026

    Summary

    OpenTelemetry conventions for recording generative AI model calls, agent operations and Model Context Protocol activity as spans (timed operations), metrics and events. They are still at Development status. Introduced in 2024, they moved to a dedicated repository in 2026.

  • Agentic AI Foundation (AAIF)

    Linux Foundation · 2025 · Organization Link checked 20 Oct 2026

    Summary

    Linux Foundation body formed in December 2025 to host open agentic AI projects. Its first projects were Anthropic's Model Context Protocol, Block's goose and OpenAI's AGENTS.md. Its working groups include Identity & Trust and Observability & Traceability.

  • Announcing Microsoft Entra Agent ID: Secure and manage your AI agents

    Microsoft · 2025 · Project Link checked 20 Oct 2026

    Summary

    Microsoft's announcement of the Entra Agent ID public preview. The preview lists agent identities created in Copilot Studio and Azure AI Foundry in one directory in the Entra admin center. Microsoft said it planned to add authentication, authorization and access governance for agents.

  • Model AI Governance Framework for Agentic AI

    IMDA (Singapore) · 2026 · Report Link checked 20 Oct 2026

    Summary

    IMDA framework for organizations deploying AI agents, first released in January 2026 and updated to version 1.5 in May 2026. It recommends giving each agent a unique, cryptographically verifiable identity tied to a supervising agent, human user or department. It also recommends human approval at significant checkpoints, and continuous monitoring and logging of agent behavior after deployment.

Verifiable evaluation & audits 19

You trust: the examiner and the access it had

  • Black-Box Access is Insufficient for Rigorous AI Audits

    Stephen Casper et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Argues that white-box and outside-the-box access allow substantially more scrutiny than black-box queries. White-box access lets auditors examine a model's internals; outside-the-box access covers information such as training data and documentation. The paper also discusses technical, physical and legal safeguards for audits with deeper access.

  • Structured access: an emerging paradigm for safe AI deployment

    Toby Shevlane · 2022 · Paper Link checked 20 Oct 2026

    Summary

    Describes structured access, in which developers let others interact with an AI system in controlled ways, typically through cloud interfaces, instead of releasing it openly.

  • Frontier AI Auditing: Toward Rigorous Third-Party Assessment of Safety and Security Practices at Leading AI Companies

    Miles Brundage et al. · 2026 · Paper Link checked 20 Oct 2026

    Summary

    Proposes rigorous third-party auditing of frontier AI developers' safety and security claims. It also proposes four AI Assurance Levels (AALs), where higher levels give more confidence in an audit's findings. It recommends AAL-1 as a baseline and AAL-2 as a near-term goal for the most advanced developers.

  • Verifiable evaluations of machine learning models using zkSNARKs

    Tobin South et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Packages zk-SNARK proofs of a model's outputs on datasets into evaluation attestations. Each attestation shows that a model with fixed, private weights achieves stated performance or fairness metrics.

    Verifiable evaluation & auditsVerifiable inference & computation

  • Trustless Audits without Revealing Data or Models

    Suppakit Waiwitlikhit et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    ZkAudit protocol, in which providers publish commitments, cryptographic values that bind them to specific datasets and model weights. They also publish a zero-knowledge proof of training. They then answer audit queries, such as copyright checks, with further proofs.

  • PySyft

    OpenMined · 2017 · Tool Link checked 20 Oct 2026

    Summary

    OpenMined's open-source library in which data scientists submit computations that data owners approve and run on private data, so that only approved results leave the owner's machine.

  • Enabling External Scrutiny of AI Systems with Privacy-Enhancing Technologies

    Kendrea Beers, Helen Toner · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Describes how OpenMined's infrastructure combines privacy-enhancing technologies (PETs) so that outsiders can scrutinize AI systems. PETs let parties compute on data while limiting what each side sees. Case studies involve the Christchurch Call and the UK AI Safety Institute.

  • Secure Enclaves for AI Evaluation

    OpenMined · 2024 · Report Link checked 20 Oct 2026

    Summary

    Pilot in which OpenMined, with staff from the UK AI Safety Institute and Anthropic, ran an AI evaluation inside an NVIDIA H100 secure enclave. GPT-2 and a five-row dataset sample stood in for confidential assets.

  • Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs

    Will Cai et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Finds that software-only methods cannot reliably detect covert model substitution in LLM APIs. In model substitution, a provider secretly serves a different model from the one it advertises. The paper evaluates trusted execution environments (TEEs) as a way to guarantee model integrity.

    Verifiable evaluation & auditsVerifiable inference & computation

  • Proving Test Set Contamination in Black Box Language Models

    Yonatan Oren et al. · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Statistical test that can prove test-set contamination, meaning that a benchmark's test items were in a model's training data. It needs neither the training data nor the weights. It checks whether the model finds the benchmark's examples more likely in their original order than in shuffled orders.

  • The Leaderboard Illusion

    Shivalika Singh et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Documents undisclosed private testing and selective score disclosure on Chatbot Arena, including 27 private variants that Meta tested before the Llama 4 release.

  • Inspect

    UK AI Security Institute and Meridian Labs · 2024 · Tool Link checked 20 Oct 2026

    Summary

    Open-source framework from the UK AI Security Institute and Meridian Labs for building and running LLM evaluations. An evaluation combines a dataset, a solver that gets the model's answers and a scorer that grades them. The framework supports agents, tool calling and sandboxed execution of model-written code, and offers more than 200 prebuilt evaluations.

  • Holistic Evaluation of Language Models

    Percy Liang et al. (Stanford CRFM) · 2022 · Benchmark Link checked 20 Oct 2026

    Summary

    Stanford CRFM benchmark that evaluated 30 language models on 42 scenarios under standardized conditions. It measured seven metrics, including accuracy, calibration, robustness, fairness and efficiency. It also released all raw prompts and completions.

  • Language Model Evaluation Harness

    EleutherAI · 2020 · Tool Link checked 20 Oct 2026

    Summary

    EleutherAI's open-source framework for testing generative language models on more than 60 standard academic benchmarks with publicly available prompts. It aims to make results reproducible and comparable across papers.

  • A Safe Harbor for AI Evaluation and Red Teaming

    Shayne Longpre et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Argues that AI companies' terms of service and their enforcement deter good-faith safety research. It proposes that major developers commit to legal and technical safe harbors. These would protect public-interest evaluation and red teaming from account suspension and legal reprisal.

  • In-House Evaluation Is Not Enough: Towards Robust Third-Party Flaw Disclosure for General-Purpose AI

    Shayne Longpre et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Proposes three measures. Researchers would use standardized AI flaw reports and rules of engagement. Providers of general-purpose AI systems would run flaw disclosure programs with legal safe harbors. Infrastructure would coordinate how flaw reports reach the many stakeholders who may be affected.

  • ISO/IEC 42006:2025 Information technology - Artificial intelligence - Requirements for bodies providing audit and certification of artificial intelligence management systems

    ISO/IEC · 2025 · Standard Link checked 20 Oct 2026

    Summary

    International Standard, published in July 2025, for bodies that audit and certify AI management systems against ISO/IEC 42001. It adds requirements to those of ISO/IEC 17021-1. It can serve as a criteria document for accrediting such bodies.

  • AI Verify Foundation

    IMDA (Singapore) · 2023 · Organization Link checked 20 Oct 2026

    Summary

    Not-for-profit subsidiary of Singapore's Infocomm Media Development Authority (IMDA), launched in June 2023. It develops open-source AI testing tools, such as the AI Verify toolkit and Project Moonshot. It also runs an accreditation program for third-party AI testing firms.

  • CAISI Evaluation of DeepSeek AI Models Finds Shortcomings and Risks

    NIST CAISI · 2025 · Report Link checked 20 Oct 2026

    Summary

    NIST's Center for AI Standards and Innovation (CAISI) summarizes its evaluation of DeepSeek R1, R1-0528 and V3.1. It compared them with U.S. reference models on 19 public and private benchmarks. CAISI reports that the DeepSeek models performed worse, cost more and were more susceptible to agent hijacking and jailbreaking.

Governance & compute verification 18

You trust: the examiner and the access it had

  • Computing Power and the Governance of Artificial Intelligence

    Girish Sastry et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Argues that AI compute is detectable, excludable (access to it can be withheld) and quantifiable, which makes it a lever for regulatory visibility, resource allocation and enforcement. It also warns of privacy, economic and centralization risks.

  • What does it take to catch a Chinchilla? Verifying Rules on Large-Scale Neural Network Training via Compute Monitoring

    Yonadav Shavit · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Proposes on-chip weight snapshots, training-run records and chip supply-chain monitoring so that governments can verify that no actor ran a prohibited large training run.

  • Verifying International Agreements on AI: Six Layers of Verification for Rules on Large-Scale AI Development and Deployment

    Mauricio Baker et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Report finding that states could eventually verify compliance with rules on large-scale AI development through six largely independent approaches, from chip security features to whistleblower programs.

  • Mechanisms to Verify International Agreements About AI Development

    Aaron Scher, Lisa Thiergart · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Overview of verification approaches for three example policy goals. It argues that more access, such as physical inspections of data centers, can often substitute for technical mechanisms that are still immature.

  • Nuclear Arms Control Verification and Lessons for AI Treaties

    Mauricio Baker · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Case study of verification in three types of nuclear arms control agreements. It draws lessons for agreements on AI development that relies on thousands of specialized chips.

  • Hardware-Enabled Mechanisms for Verifying Responsible AI Development

    Aidan O'Gara et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Workshop-based overview of hardware-enabled mechanisms (HEMs) for reporting training compute, cluster configuration or location in a verifiable way. HEMs are features built into AI chips or servers. The overview also covers open questions about implementing them.

  • Hardware-Enabled Governance Mechanisms: Developing Technical Solutions to Exempt Items Otherwise Classified Under Export Control Classification Numbers 3A090 and 4A090

    Gabriel Kulp et al. (RAND) · 2024 · Report Link checked 20 Oct 2026

    Summary

    RAND working paper introducing hardware-enabled governance mechanisms for AI chips, the export-control objectives they could support, and the attacks they would need to withstand.

  • Secure, Governable Chips: Using On-Chip Mechanisms to Manage National Security Risks from AI & Advanced Computing

    Onni Aarne, Tim Fist, Caleb Withers (CNAS) · 2024 · Report Link checked 20 Oct 2026

    Summary

    CNAS report proposing on-chip governance mechanisms for data-center AI chips, such as privacy-preserving verification and operating licenses that a chip needs to keep running. It names export control enforcement as a near-term application.

  • Location Verification for AI Chips

    Asher Brass (IAPS) · 2025 · Report Link checked 20 Oct 2026

    Summary

    Issue brief proposing delay-based location verification for AI chips. A chip's response times to trusted landmark servers set an upper limit on its distance from them. The brief estimates the cost of a firmware update and a landmark network.

  • Flexible Hardware-Enabled Guarantees for AI Compute

    James Petrie et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    First paper in a three-part series proposing flexible hardware-enabled guarantees (flexHEG). The proposal places an auditable guarantee processor in a tamper-protective enclosure to monitor the use of AI accelerators.

  • Tools for Verifying Neural Models' Training Data

    Dami Choi, Yonadav Shavit, David Duvenaud · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Introduces proof-of-training-data protocols, which let a model trainer show which data produced a set of weights. Examples include pre-committed random seeds and checks based on models' tendency to temporarily overfit their training data. In the authors' experiments, these protocols caught all known proof-of-learning attacks.

  • Opt-In NVIDIA Software Enables Data Center Fleet Management

    NVIDIA · 2025 · Report Link checked 20 Oct 2026

    Summary

    NVIDIA's announcement of an opt-in, customer-installed service that streams GPU telemetry (operating data) to a fleet dashboard. NVIDIA states that its GPUs have no hardware tracking technology, kill switches or backdoors.

  • Toward Trustworthy AI Development: Mechanisms for Supporting Verifiable Claims

    Miles Brundage et al. · 2020 · Report Link checked 20 Oct 2026

    Summary

    Multi-author report on how AI developers could make verifiable claims about the safety, security, fairness and privacy of their systems. It analyzes ten institutional, software and hardware mechanisms, such as third-party auditing, red teaming, audit trails and secure hardware for machine learning. It recommends steps to implement or improve them.

    Governance & compute verificationVerifiable evaluation & audits

  • H.R. 3447: Chip Security Act

    U.S. House of Representatives · 2025 · Standard Link checked 20 Oct 2026

    Summary

    Bill introduced in the U.S. House on 15 May 2025. It would require export-controlled advanced chips to carry location verification mechanisms before export. It would also require license holders to promptly report credible information on diversion or tampering.

  • America’s AI Action Plan

    The White House · 2025 · Report Link checked 20 Oct 2026

    Summary

    White House policy plan. Its recommended actions include exploring location verification features on advanced AI chips to enforce export controls. They also include having NIST's Center for AI Standards and Innovation (CAISI) evaluate frontier AI systems for national security risks and assess risks from adversaries' AI systems.

    Governance & compute verificationVerifiable evaluation & audits

  • Tracking AI Chips: Assessing Location Verification as an Export Control Enforcement Tool

    Jacob Feldgoise, Kyle Miller, Hanna Dohmen (CSET) · 2026 · Report Link checked 20 Oct 2026

    Summary

    CSET report that assesses methods for verifying the location of AI chips to enforce export controls. It judges the methods on verifiability, accuracy, security and repeatability. It finds that the most feasible approach is ping-based verification (timing a chip's network replies) supplemented by physical inspections. The report also sets out that approach's limitations.

  • Verification for International AI Governance

    Ben Harack et al. (Oxford Martin AIGI) · 2025 · Report Link checked 20 Oct 2026

    Summary

    Report finding that many international AI agreements could be verified without speculative technology. It finds that rules on data-center AI development appear verifiable within a few years, given dedicated verification hardware and serious effort. It also finds that detailed rules on mobile AI-enabled devices in sensitive domains, such as weapons, face severe political barriers.

  • How to Catch a GPU: A Taxonomy of Verification and Enforcement Mechanisms for International AI Agreements

    Raymond Koopmanschap, Otto Barten · 2026 · Paper Link checked 20 Oct 2026

    Summary

    Taxonomy for assessing whether proposed international AI agreements can be enforced. It splits compliance into three problems: preventing uncontrolled resource acquisition, detecting all capacity outside the control regime, and preventing escape from the regime. It also defines an enforcement breaking point, the compute threshold at which a policy loses its effectiveness.

Verifiable inference & computation 21

You trust: an honest checker or the proof system and the statement proven

  • A Survey of Zero-Knowledge Proof Based Verifiable Machine Learning

    Zhizhi Peng et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Survey of zero-knowledge machine learning (zkML) research from June 2017 to August 2025. In zkML, zero-knowledge proofs let others check a machine-learning computation without seeing secrets such as model weights. The survey groups the work into verifiable training, testing and inference, and analyzes bottlenecks such as the cost of generating proofs.

  • SafetyNets: Verifiable Execution of Deep Neural Networks on an Untrusted Cloud

    Zahra Ghodsi, Tianyu Gu, Siddharth Garg · 2017 · Paper Link checked 20 Oct 2026

    Summary

    Interactive-proof protocol that lets a client check that an untrusted cloud ran neural-network inference correctly. It applies to networks that can be expressed as arithmetic circuits, built only from additions and multiplications.

  • Scaling up Trustless DNN Inference with Zero-Knowledge Proofs

    Daniel Kang et al. · 2022 · Paper Link checked 20 Oct 2026

    Summary

    Presents a zk-SNARK proof of valid inference for an ImageNet-scale model. A zk-SNARK is a short zero-knowledge proof that is quick to verify. The paper also gives protocols that use such proofs to verify the predictions and accuracy of ML services.

  • zkLLM: Zero Knowledge Proofs for Large Language Models

    Haochen Sun, Jason Li, Hongyang Zhang · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Zero-knowledge proof system for large language models. It handles non-arithmetic operations with a lookup argument, which checks values against a precomputed table. A dedicated proof handles attention. The authors report proving a 13-billion-parameter model's inference in under 15 minutes.

  • DeepProve: Verifiable End-to-End Large Language Model Inference

    Nicolas Gailly et al. · 2026 · Paper Link checked 20 Oct 2026

    Summary

    Zero-knowledge system, built on the sum-check protocol and lookup arguments, that proves all the tokens generated for a prompt. It was demonstrated on GPT-2 at about 174 proven tokens per minute and on Gemma 3 at about 86.

  • EZKL

    Zkonduit · 2022 · Tool Link checked 20 Oct 2026

    Summary

    Library and command-line tool that turns models and other computational graphs exported as ONNX into zk-SNARK circuits. With these circuits, the models' inference can be proven and verified. EZKL can be used from Python, JavaScript or the command line.

  • TOPLOC: A Locality Sensitive Hashing Scheme for Trustless Verifiable Inference

    Jack Min Ong et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    The inference provider commits to locality-sensitive hashes of intermediate activations, the values computed inside the model. These hashes stay similar when the activations are similar. A validator can then detect changes to the model, prompt or numerical precision while tolerating differences across GPU types.

  • Verde: Verification via Refereed Delegation for Machine Learning Programs

    Arasu Arun et al. · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Refereed-delegation protocol for ML training and inference. When compute providers disagree, a referee narrows the dispute to a single operator. The protocol comes with RepOps, a library of operators that return bit-for-bit identical results when rerun.

  • Model Equality Testing: Which Model Is This API Serving?

    Irena Gao, Percy Liang, Carlos Guestrin · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Frames the detection of quantized (reduced-precision), watermarked or fine-tuned models behind an API as a two-sample test. Such a test asks whether two sets of outputs come from the same distribution. The paper reports that 11 of 31 tested endpoints served distributions different from Meta's reference weights.

    Verifiable inference & computationVerifiable evaluation & audits

  • IMMACULATE: A Practical LLM Auditing Framework via Verifiable Computation

    Yanpei Guo et al. · 2026 · Paper Link checked 20 Oct 2026

    Summary

    Auditing framework that checks a small fraction of API requests with verifiable computation, in which the provider returns evidence that a result is correct. It looks for model substitution, quantization abuse and token overbilling, without relying on trusted hardware.

    Verifiable inference & computationVerifiable evaluation & audits

  • Proof-of-Learning: Definitions and Practice

    Hengrui Jia et al. · 2021 · Paper Link checked 20 Oct 2026

    Summary

    Introduces proof-of-learning, a record of checkpoints (weights saved during training) and training metadata. It lets a verifier check that a party performed the training that produced a set of weights.

  • Optimistic Verifiable Training by Controlling Hardware Nondeterminism

    Megha Srivastava, Simran Arora, Dan Boneh · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Uses higher-precision training and shared rounding decisions to control nondeterminism, the small differences in numerical results across GPU types. An auditor can then replicate training exactly and contest a trainer's result.

  • Defeating Nondeterminism in LLM Inference

    Horace He, Thinking Machines Lab · 2025 · Report Link checked 20 Oct 2026

    Summary

    Shows that LLM inference servers return different outputs for the same input mainly because their kernels lack batch invariance while server load varies. Without batch invariance, a request's result depends on how many other requests are processed with it. The post demonstrates batch-invariant kernels that made 1,000 temperature-zero completions identical.

  • Pinocchio: Nearly Practical Verifiable Computation

    Bryan Parno et al. · 2013 · Paper Link checked 20 Oct 2026

    Summary

    Verifiable computation system that compiles a subset of C into a protocol. A worker returns a 288-byte proof of correct execution. Anyone holding the public verification key can check it, typically in about 10 milliseconds. An optional zero-knowledge variant adds little extra cost.

  • zkCNN: Zero Knowledge Proofs for Convolutional Neural Network Predictions and Accuracy

    Tianyi Liu, Xiang Xie, Yupeng Zhang · 2021 · Paper Link checked 20 Oct 2026

    Summary

    Zero-knowledge proof scheme built on a new sum-check protocol for convolutions. A model owner can use it to prove that a convolutional neural network's prediction came from a secret model, without revealing the model. The scheme can also prove the model's accuracy on a public dataset. For VGG16, the proof took 88.3 seconds to generate and 59.3 milliseconds to verify.

    Verifiable inference & computationVerifiable evaluation & audits

  • Proofs, Arguments, and Zero-Knowledge

    Justin Thaler · 2022 · Course Link checked 20 Oct 2026

    Summary

    Free draft textbook on interactive proofs, arguments and zero-knowledge proofs. Topics include the sum-check protocol, the Fiat-Shamir transformation, polynomial commitments and SNARKs built from polynomial interactive oracle proofs (IOPs). It links to video lectures.

  • Proof-of-Learning is Currently More Broken Than You Think

    Congyu Fang et al. · 2022 · Paper Link checked 20 Oct 2026

    Summary

    Presents spoofing attacks on proof-of-learning: the attacker forges a training record for weights it did not train. The attacks reproduce across verification settings at a fraction of the cost of earlier attacks. The authors argue that a provably robust proof-of-learning verifier requires a better understanding of optimization in deep learning.

  • Experimenting with Zero-Knowledge Proofs of Training

    Sanjam Garg et al. · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Defines zero-knowledge proofs of training (zkPoT). Such a proof lets a model owner prove that a model was trained according to a specification, without revealing the data or the model. The authors implement a protocol for logistic regression that combines MPC-in-the-head with zk-SNARKs, and benchmark it on a 4 GB dataset.

  • SVIP: Towards Verifiable Inference of Open-source Large Language Models

    Yifan Sun et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Protocol for checking whether a decentralized computing provider ran the requested open-source LLM. The provider returns hidden-layer representations, the model's internal values, along with the generated text. The user checks them with a trained proxy task and a secret mechanism. The authors report false negative rates below 5% and false positive rates below 3%.

  • opML: Optimistic Machine Learning on Blockchain

    KD Conway et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Optimistic approach to on-chain machine-learning inference. Instead of zero-knowledge proofs, it relies on an interactive fraud-proof protocol similar to optimistic rollups. A result stands unless someone challenges it. The authors report running a 7B-parameter LLaMA model on a standard PC without a GPU.

  • K2 Vendor Verifier

    Moonshot AI · 2025 · Tool Link checked 20 Oct 2026

    Summary

    Moonshot AI tool that sends 4,000 tool-calling requests to third-party providers of its Kimi K2 models. It measures how closely their decisions on whether to call a tool match Moonshot's official API. It also measures how often their tool-call JSON passes schema validation, a check of its format. The test is now one of the benchmarks in Moonshot's broader Kimi Vendor Verifier.

Formal verification 23

You trust: the proof system and the statement proven

  • Towards Verified Artificial Intelligence

    Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry · 2016 · Paper Link checked 20 Oct 2026

    Summary

    Agenda paper that defines verified AI from the perspective of formal methods, mathematical techniques for specifying and verifying systems. It sets out five challenges and five corresponding principles.

  • Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems

    David Dalrymple et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    Defines guaranteed safe AI as a family of approaches that combine a world model, a safety specification and a verifier. The world model describes mathematically how the AI system affects the outside world. The verifier provides an auditable proof certificate that the system meets the specification relative to the world model.

  • Provably safe systems: the only path to controllable AGI

    Max Tegmark, Steve Omohundro · 2023 · Paper Link checked 20 Oct 2026

    Summary

    Position paper arguing that artificial general intelligence should be built to provably satisfy human-specified requirements. The authors propose using advanced AI for formal verification and for mechanistic interpretability, the study of a model's internal mechanisms.

  • Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

    Guy Katz et al. · 2017 · Paper Link checked 20 Oct 2026

    Summary

    Simplex-based SMT technique for neural networks with ReLU activations. It either proves that a network has a given property or finds a counterexample. It was evaluated on networks from a prototype airborne collision-avoidance system (ACAS Xu).

  • alpha-beta-CROWN

    Verified-Intelligence · 2021 · Tool Link checked 20 Oct 2026

    Summary

    GPU-accelerated neural-network verifier based on linear bound propagation and branch and bound. Its README lists it as the winner of every annual neural-network verification competition (VNN-COMP) from 2021 to 2026.

  • The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results

    Konstantin Kaulen et al. · 2025 · Report Link checked 20 Oct 2026

    Summary

    Report on the 2025 edition of the annual competition that compares neural-network verifiers on shared ONNX and VNN-LIB benchmarks. Eight teams took part.

  • Lean

    Lean FRO · 2013 · Tool Link checked 20 Oct 2026

    Summary

    Open-source programming language and proof assistant, software that checks every step of a proof. It is used for formally verified code and machine-checked mathematics, and is a common target for AI-generated proofs.

  • Dafny

    Dafny project · Tool Link checked 20 Oct 2026

    Summary

    Verification-aware programming language whose static verifier checks code against its specifications before it runs. Dafny programs compile to languages such as C#, Java, JavaScript, Go and Python.

  • Verus

    verus-lang · 2021 · Tool Link checked 20 Oct 2026

    Summary

    Tool for verifying Rust code in which developers write specifications and proofs that automated solvers check for all possible executions.

  • DafnyBench: A Benchmark for Formal Software Verification

    Chloe Loughridge et al. · 2024 · Benchmark Link checked 20 Oct 2026

    Summary

    Benchmark of over 750 Dafny programs that tests whether language models can generate the hints the Dafny verifier needs. At release, the best model and prompt succeeded on 68 percent of them.

  • A benchmark for vericoding: formally verified program synthesis

    Sergiu Bursuc et al. · 2025 · Benchmark Link checked 20 Oct 2026

    Summary

    Benchmark of 12,504 formal specifications in Dafny, Verus/Rust and Lean for generating formally verified code. Off-the-shelf models succeeded 82, 44 and 27 percent of the time in those three languages, respectively.

  • Vero: Can AI Agents Build Formally Verified Software Repositories?

    Zhe Ye et al. · 2026 · Benchmark Link checked 20 Oct 2026

    Summary

    Repository-scale benchmark of 43 multi-module Lean 4 tasks, in which an agent must write both the implementation and its proof. Agents may also prove that a specification cannot be satisfied. The strongest agent fully solved 27 tasks.

  • Safeguarded AI

    ARIA · Project Link checked 20 Oct 2026

    Summary

    Program of the UK's Advanced Research and Invention Agency (ARIA), backed by £59m. It is building an open-source toolkit with which AI agents produce formally verified artifacts, and is applying it mainly to cybersecurity.

  • Olympiad-level formal mathematical reasoning with reinforcement learning

    Thomas Hubert et al. (Google DeepMind) · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Describes AlphaProof, an AlphaZero-inspired agent that learns to find formal proofs in Lean through reinforcement learning. It trains on millions of problems that were automatically translated into Lean. At the 2024 International Mathematical Olympiad, it solved three of the five non-geometry problems. Together with AlphaGeometry 2, it reached a silver-medal-equivalent score.

  • Aristotle: IMO-level Automated Theorem Proving

    Tudor Achim et al. (Harmonic) · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Harmonic's theorem-proving system, which produced formal solutions to five of the six problems of the 2025 International Mathematical Olympiad. It searches over Lean tactics, the commands that build a proof, with Monte Carlo graph search. Its informal reasoning system drafts and formalizes lemmas, and a separate solver handles geometry.

  • DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition

    Z. Z. Ren et al. (DeepSeek-AI) · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Open-source Lean 4 theorem-proving model. Its cold-start data, used in the first training stage, come from a pipeline in which DeepSeek-V3 decomposes problems into subgoals. Reinforcement learning follows. The 671B-parameter model reaches an 88.9% pass ratio on MiniF2F-test and solves 47 of 658 PutnamBench problems.

  • Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

    Luoxin Chen et al. (ByteDance Seed) · 2025 · Paper Link checked 20 Oct 2026

    Summary

    Lean theorem-proving model that refines whole proofs using Lean feedback, proved lemmas and self-summarization. It works with the Seed-Geometry engine. The authors report fully proving five of the six 2025 International Mathematical Olympiad problems, one of them after the submission deadline. They also report proving 78.1% of formalized past IMO problems.

  • Certified Adversarial Robustness via Randomized Smoothing

    Jeremy M. Cohen, Elan Rosenfeld, J. Zico Kolter · 2019 · Paper Link checked 20 Oct 2026

    Summary

    Proves a tight ℓ2-norm robustness guarantee for classifiers smoothed with Gaussian noise, which predict by majority vote over noisy copies of an input. For example, it certifies 49% top-1 accuracy on ImageNet under perturbations of ℓ2 norm below 0.5. Because the guarantee is computed by Monte Carlo sampling, it holds only with high probability.

  • Marabou 2.0: A Versatile Formal Analyzer of Neural Networks

    Haoze Wu et al. · 2024 · Paper Link checked 20 Oct 2026

    Summary

    System description of version 2.0 of Marabou, an open-source verifier that checks properties of neural networks. It solves linear and non-linear constraints with an SMT-based procedure. The new version can produce proof certificates for queries that have no solution. It also handles more activation functions and accepts queries through a richer Python API.

  • Automated Reasoning checks is now available in Amazon Bedrock Guardrails

    Amazon Web Services · 2025 · Report Link checked 20 Oct 2026

    Summary

    AWS announcement that Automated Reasoning checks in Amazon Bedrock Guardrails are generally available. The safeguard uses formal verification techniques to check generative AI outputs against an Automated Reasoning policy. The policy's rules are extracted from a customer's own documents.

  • The Rocq Prover

    Inria · 1984 · Tool Link checked 20 Oct 2026

    Summary

    Interactive theorem prover and dependently typed programming language, formerly the Coq Proof Assistant. It is used to write formal specifications and machine-checked proofs that programs meet them. It can also extract executable OCaml or Haskell code from specifications.

  • Isabelle

    University of Cambridge and Technical University of Munich · 1986 · Tool Link checked 20 Oct 2026

    Summary

    Generic proof assistant, used mainly as Isabelle/HOL for higher-order logic. It checks formal proofs about mathematics and about the correctness of hardware, software and protocols. Through Sledgehammer, it can call external automated provers. It comes with the Archive of Formal Proofs, a collection of proofs checked in Isabelle.

  • Theorem Proving in Lean 4

    Jeremy Avigad et al. · 2021 · Course Link checked 20 Oct 2026

    Summary

    Book on writing definitions and machine-checked proofs in Lean 4, written with contributions from the Lean community. It covers dependent type theory, propositions and proofs, tactics, inductive types, structures and type classes.