FlashProve: ZK Proofs for AI Inference, Claude-Written, Lean-Verified

Background and Phenomena: You Don’t Know if the Reply Comes from the Model You Chose

On November 4, 2026, Anthropic released a research blog post titled “Progress on provable inference for large language models,” announcing a system called FlashProve. Five artifacts were also made open source: the blog itself, technical reports, protocol specifications, executable code (a prover and two verifiers), Lean proofs, and a theorem-interaction visualization tool. All code, proofs, and documentation are licensed under Apache 2.0. The accompanying repository anthropics/FlashProve was created on October 30, 2026, and as of November 5, it had received 781 stars. The version file indicated 0.16.0; the blog had 155 HN entries and 77 comments.

The questions raised by the blog were straightforward: when users request responses from models, there is no way to confirm that the reply indeed comes from the model they selected. Routing services may secretly switch to cheaper models to save money, and attackers may tamper with token flows; inferring reliability from output quality makes responses unreliable, and even the best answers cannot prove one’s identity. Independent evaluators need to know that the model being evaluated is the one running online, and users using third-party routing need to confirm that the tokens come from models they paid for.

The second breakdown point is the author lineup and Claude’s role in it. The blog is signed by a mix of academia and cryptography startup circles: two people from Anthropic, three from EPFL, and researchers from MIT, StarkWare, Succinct, and RESI. More striking is the blog’s self-description: “Claude improved zkSNARK for reasoning,” creating a system much faster than existing open-source systems; the protocol specification document in the five artifacts clearly states it was written by Claude. Anthropic also acknowledges the risks and countermeasures of this approach: Claude excels at optimization, but decisions in large and complex systems are often difficult to evaluate. The countermeasure is to write claimed security guarantees as auditable top-level propositions in Lean (a formal verification language).

The first line of the README describes itself as “Research artifacts: no maintenance, no contributions.” The blog also explicitly states that this is an intermediate progress, not a completed research agenda, with the purpose of allowing others to take the improvements.

Architecture and Technical Principles: Three Steps of Commit, Prove, Verify

The core of FlashProve is zkSNARK-based provable reasoning, which is divided into three steps (as stated in the README). The first step, commit, involves the service provider issuing a commitment ID, binding a set of weights, with the weights themselves being confidential. All public values of the dependent weights are masked, except for the list declared in docs/what-is-not-hidden.md; the design goal is clearly stated: hiding weights is the goal, not hiding the architecture. The second step, prove, involves each reply being proven by the service provider’s GPU. The third step, verify, allows anyone to use the C++ verifier cp_verify to verify in seconds on a regular CPU that “this reply indeed comes from the promised model,” without needing weights throughout the process.

The Lean part is the other half of the repository’s focus. There are 30,902 files in total after local cloning, including 29,563 .lean files and only 185 .py files, with a total size of 723MB. The directory contains prover, verifier, lean, paper (technical report PDFs), docs (19 articles), guide (8 articles), tests, toy, scales, etc. lean/THEOREM.md lists six theorems, all targeting the same set of committer, prover, and verifier, valid for each public setup: sound (the probability that a cheating party can pass the verifier under q hash queries is no more than approximately q/2^124 + 2^-101; the original text notes “this is a boundary, not a security level”); soundAndBinding (no one can manipulate the commitments into another set of weights, except for a probability of approximately q/2^124 + 2^-100); completeOnCanServe (the probability that an honest proof is wrongly rejected for service requests does not exceed 2^-40); zeroKnowledgeOnCanServe (leaking the boundary within 2^64 hash queries and 688,127 responses does not exceed 2^-154; simulators cannot obtain weights); refusedHandsOutNoProof (rejected requests can only return an empty proof, but “whether the rejection is correct” is not within the scope of the proof); repliesFit (the consistency count between 688,127 responses and the number of tables).

Two boundaries deserve mention, both as self-proclaims of the repository. First, all six theorems require “exact matching,” and the verifier does not check this: if a service provider changes the public file strategy after seeing a request, the theorem does not apply. Second, all test suites use synthetic weights; SUITE.md states: passed tests only indicate that the program provides expected answers for synthetic inputs, and do not reveal more about reliability or secrecy.

Key Data: 110 tokens/s, 93 times the cost, and six probability boundaries

All performance numbers come from repository guide/performance.md and README, which are official self-proclaims, with no independent reproduction available.

Object running: Llama 4 Maverick full size (400B parameter MoE), using third-party public 4-bit conversion (downloads 232GB), 1,024-token context window, and 80GB per H100 instance. Speed: prefill batch 24 hours at 111.23±0.92 tokens/s, README estimates around 110; batch 1 only 17.41; batch 64 reaches 123.31, but the repository itself notes that 80GB GPUs are unreliable for batch 64, with memory reaching 80,629/81,559 MiB; all CUDA calls failed after 8 attempts under synthetic weights.

The cost is also a self-proclaim of the repository: per GPU, it is 93.0 times slower than vLLM’s native prefill (highest load scenarios), and 71.4 times slower than vLLM’s batch 24, and this is “calculated, the best-case” without considering startup and commitment times. The baseline machine still runs FP8 with 8×H100.

Proof and storage volume: The average size of a single proof is 18.78MB; the client’s one-time download for each commitment is 6.24MB; the service provider needs to store 2.15GB per commitment. The commitment process takes about 39 minutes, and one commitment can be used multiple times; the service provider’s host memory should be at least 330GB, with 245GB of disk space. The verification cost is the most asymmetric number in the entire system: cp_verify takes about 21 seconds in a single thread, requires up to 3.53GB of memory, and does not require a GPU; the Lean version of “verifiable correctness verifier” takes about 24 minutes for a full-size proof, requiring up to 14.13GB of memory.

The repository is quite honest about its weaknesses: startup time is 68-79 seconds; after distributing the commitment cost across the first 1,000 requests, the steady-state rate is 88.81 tok/s, failing to meet the self-set goal of 100 tok/s, and performance.md directly acknowledges that it does not meet the standard.

Impact and significance: Turning “which model says” into an verifiable attribute

First, in terms of compliance and audit scenarios. The blog explicitly states that zkSNARK can be used as a tool to verify AI compliance requirements: regulators require service providers to provide certificates covering推理 requests over a certain period. Service providers cannot forge these certificates unless they are actually running the claimed model with hardware, and at the same time, regulators cannot obtain exclusive rights information. A highly praised comment on HN conveys the same idea: in compliance audits, proxy chains, and regulatory scenarios, “which model says” is itself a key attribute.

Second, the trust issue of aggregate routing. Some comments point out that aggregators like OpenRouter route requests to other models, and this mechanism can be caught; another comment provides a more specific fraud scenario: some market Claude resellers promise access but actually switch models, which can be proven to prevent such incidents. Others mention rumors that models with the same name on certain hosts perform significantly worse, possibly running an undisclosed quantitative version (the commenter believes it’s a rumor), and ask if this mechanism can catch them.

Third, open-source weight models can also use it to prove themselves. A highly praised comment that read the repository documents points out: using public weights for commitments and publishing seeds allows anyone to recalculate commitments from Hugging Face files, verifying whether the service provider runs the claimed checkpoint and quantitative bit width. This means that this mechanism serves not only closed-source manufacturers but also provides the community with a self-checking tool.

Fourth, the methodological significance of Claude writing cryptographic code with Lean as a backup is probably greater than the system itself. Translating “difficult-to-evaluate AI decisions” into verifiable top-level propositions in formal language, allowing machines to prove that they review code written by humans, is a reusable engineering paradigm when AI participates in critical infrastructure development (this is my judgment).

Controversy and risks: A PR move, or filling a vacuum?

The most vocal comments in HN’s comment section were sarcastic. The highest-rated comment considered it a PR move, with some netizens referring to previous reports, accusing the same company of quietly routing ML-related requests to weaker models, which was reported (the commenter identifies, but has not been independently verified). But another highly praised comment refuted this: switching models is precisely the most common complaint from users, and there was no verification mechanism before. If this can be implemented, it would be significant.

The debate about value goes deeper. Some believe it proves an attribute that is “a minimum requirement”: however, it doesn’t provide much useful information beyond ensuring that the model isn’t replaced with cheaper ones or bypassed by intermediaries; others initially thought it was meant to prove “correct output,” only to find it only verified which model was used, stating that if there was already distrust in the service provider, the game would have already ended. The counterargument: customers care about correctness of output, while manufacturers focus on output coming from their own models—this solution addresses the latter issue; some comments predict it will eventually be used to create FUD against cheap routing services (this is a speculation based on the reviewer’s motivation). My view: there isn’t an actual conflict between the two sides. “Correct output” and “output from the claimed model” are two independent verification issues. The former remains unresolved, and the latter currently has only cryptography as a feasible path (this is my judgment).

There are three hard boundaries to technical risks. First, the issue of precise matching: all six theorems require that the published documents be exactly consistent with the promises, but verifiers don’t check this, and service providers can change their strategies after receiving requests, falling outside the guarantee range. This is a known flaw identified by the repository. Second, the deployment threshold: the GPU stack requires x86-64 Linux 4.14+ with SHA extension, a CPU with exclusive access to an H100 80GB, CUDA 13.2 Update 2 (clearly not supporting updated toolkits), and for the real model approach, 330GB of memory and 245GB of disk space—something that individuals and small teams can hardly achieve. Third, all performance numbers are reported by the official side, with no third-party reproducibility. The 93-fold slowdown also means it’s more of an auditing tool than a production feature that can run continuously.

Conclusion and Outlook: The Repository Is Its Own Second Experiment

The core message is this: FlashProve uses zkSNARK to turn “the reply coming from the promised weight” into a proposition that anyone with a regular CPU can verify in seconds, at the cost of 70-95 times more GPU time and a deployment threshold equivalent to 330GB of memory. At the same time, it uses 29,563 Lean files to translate the question “Is Claude’s cryptographic code trustworthy?” into six auditable theorems.

It’s worth noting one phenomenon: the README includes a section titled “Built to be run by an agent.” The author assumes readers will direct their coding agent to this repository, providing directly copyable instruction text. The verification process is divided into four paths based on hardware: Path 1 requires only Linux and g++13 with 2GB of memory, takes 1-2 minutes to build, and 2 seconds to verify existing proofs; Path 2 runs toy proofs on CPU in about 1 minute; Path 3’s eight-layer composite model requires the full H100 stack, taking about 29 minutes to build; Path 4 is the real Llama 4 Maverick, taking hours. The security stance is also appropriate: root/sudo are completely prohibited throughout, and Landlock is used in the sandbox. These designs themselves are an experiment “to ensure the agent safely operates in a unfamiliar repository,” and the first reader of the repository documents may be transitioning from a human to an agent.

Two things deserve attention in the future. First, the README statement indicates that no maintenance or contributions will be accepted, and the blog encourages others to take over for improvement. It’s likely that the five artifacts of Apache 2.0 will continue to be developed by academia and cryptography startups. Whether an independent replicable implementation can emerge is a harder test than just marking it as starred. Second, whether the precise matching boundary will be addressed determines whether this mechanism can move from audit scenarios to regular production processes.

My conclusion in one sentence: FlashProve is worth dissecting, not because it has solved the problem of inference trust (it hasn’t, and the official team also admits it’s only an intermediate progress), but because it has turned two things that previously could only be guaranteed verbally into provable propositions: the identity of models and the correctness of cryptography code written by AI. The former points to the foundation of trust in the inference market, while the latter refers to the quality assurance methods of the AI programming era.

Reference Sources

• Anthropic research blog “Progress on provable inference for large language models”: anthropic.com/research/provable-inference (published on 2026-11-04; Claude-related statements are all from the blog’s own description)
• HN entry: story 50368626 (155 ▲ / 77 comments, snapshot on 2026-11-05)
• Repository: github.com/anthropics/FlashProve (781★ / Apache 2.0 / created on 2026-10-30 / VERSION 0.16.0, snapshot on 2026-11-05)
• Local shallow clone verification (tested on 2026-11-05, no code from the repository ran): README.md, guide/performance.md, lean/THEOREM.md, SUITE.md, docs/, AGENTS.md; 30,902 files / 723MB for local statistics
• HN comment pool: hn-provable.json (47 records, all text excerpts without direct quotes)

Author: Yongliang