Version 0.16.0 · A research artifact: not maintained, not accepting contributions. · Apache 2.0

FlashProve lets an AI provider prove which model answered a request, without revealing the model's weights.

• Commit. The provider publishes a commitment ID, which binds it to one set of weights. The weights themselves stay secret: every published value that depends on them is masked, except a declared list.
• Prove. For each reply, the provider's GPU produces a proof that the reply is the committed model's output.
• Verify. Anyone can check the proof on an ordinary CPU in seconds with cp_verify, without the weights.

FlashProve runs Llama 4 Maverick at full size, with a 1,024-token context window, on a single NVIDIA H100. The prover reaches about 110 tokens/second of prefill at 24 requests per batch (Performance).

The protocol's soundness is proved in Lean 4. A provider that tries to pass off output that is not the committed model's is caught, except with probability about q/2^124 + 2^-101 after q hash queries. lean/THEOREM.md has the theorem and how to check it.

Building FlashProve, running it and checking its output take long builds and many exact comparisons. That work is meant for a coding agent. Point yours at this repository with:

Read README.md in the FlashProve repository, starting at "For agents", and AGENTS.md. Working from
the repository root as an ordinary (non-root) user, build the verifier, check the stored example
proof, and report the exit code and last line. Then tell me which other routes (toy proofs on CPU,
small model on an H100, full size) this machine can run, and ask me before starting any of them.

Run everything from the repository root as an ordinary user, never as root or under sudo. Only installing system packages needs root, so ask your user to do that. If root is the only account, create one first (how). Also read AGENTS.md for the rules on reporting results.

GPU stack (routes 3 and 4) is the only supported platform for the prover:

• x86-64 Linux 4.14 or later, on a CPU with the SHA extensions.
• One NVIDIA H100 80 GB, used by nothing else.
• CUDA 13.2 Update 2 (nvcc 13.2.86) on PATH. prover/docs/build.md prints the pip lines that install it.
• gcc and g++ 13 first on PATH; binutils, flock, python3.
• The repository and work directories on a local disk.

On minimal Ubuntu 24.04, route 1 and 2 dependencies are (needs root):

apt-get update && apt-get install -y --no-install-recommends g++ make python3 unzip

verifier/build.sh

It is silent for 1–2 minutes, then prints a line starting THE VERIFIER IS BUILT: and exits 0. A line starting build.sh: note: is a warning: quote it in your report. If your tool calls time out, run the build in the background:

echo "build started" >> verifier-build.log; nohup bash -c 'verifier/build.sh; echo "exit code $?"' >> verifier-build.log 2>&1 &

Then poll tail -n 2 verifier-build.log until the last line starts exit code. Don't start a second build meanwhile.

bin/cp_verify examples/accepted-proof/config examples/accepted-proof/ivk examples/accepted-proof/example.req examples/accepted-proof/example.y examples/accepted-proof/example.proof -id "$(cat examples/accepted-proof/ID.txt)"

Expect last line YES, exit code 0. This example is a small model with synthetic weights, so it shows only that the verifier works, not anything about a served model.

W=$(mktemp -d) && LOOK="$W/look" && echo "LOOK=$LOOK"
blocks/first_look.sh "${LOOK:?first run the line with mktemp}"

Expect exit code 0, and the third line from the end starts AS EXPECTED: the honest copy was accepted.

examples/quickstart-gpu.sh

This builds cp_verify, cp_commit and cp_prove, then commits, proves one 64-token request and verifies it.

• It can be silent for over 15 minutes. It logs to quickstart-gpu.log in a directory it names first.
• Success is exit code 0 and a line starting quickstart-gpu: all steps ended as expected.
• Also check that every Compiled by line ends in release 13.2, V13.2.86. A newer nvcc does not stop the build, but it is not supported.

Full size, after that build:

W=$(mktemp -d) && WORK="$W/example" && echo "WORK=$WORK"
prover/examples/run_target_example.sh target_full_f2 "${WORK:?first run the line with mktemp}"

Expect status 0, a proof of work: line, then YES. Progress goes to $WORK/cp_commit.log. With too little memory it exits with code 2 at the start.

For the real Maverick weights, see route 4 and examples/maverick/run.sh. To commit to and serve a model of your own, see Serving and the provider's duties. Those pages are required reading before using weights that must stay secret.

bin/cp_verify CONFIG_DIR PUBLIC_KEY_DIR REQUEST_FILE TOKEN_FILE PROOF_FILE -id COMMITMENT_ID

• The commitment ID: get it from a party your user trusts, never from the server being checked or from files sent with the proof. The stored examples are the only exception.
• The request file: build it yourself (Verify a proof).
• What to read: the exit code together with the last line.

verifier/docs/output.md has the full table. integrations/check_proof.py wraps the call and the comparisons.

D=$(mktemp -d) && ./run_suite.py cpu "$D/work"

These are the CPU tests. They overwrite bin/cp_verify and bin/weight_sums.

• Exit 0 means a pass; 77 means tools are missing.
• Exit 3 means a test saw something false accepted: report it per SECURITY.md.

See SUITE.md.

• Never get past an error with sudo, chmod, chown, rm, or by editing a source file. Stop and ask your user.
• Don't build prover/ unless the task needs it.
• Report the exact command, the exit code and the full last line. For an accepted proof, also report the commitment ID you passed and the covered: and result-v1 lines.

• Guides: Getting started, How it works, Verify a proof, Serving, What is proved, Weight hiding, Known limits, Performance, Terms.
• Reference: docs, glossary, protocol, format spec, Lean library, Lean verifier, tests, paper, SECURITY.md.
• Examples and checks: the stored example, a full-size proof, rejected proofs, faults, the integration's limits, checking the Lean library, its results.
• Limits: docs/limits.md, docs/limits-further.md, the table of all rows, lean/LIMITS.md, known errors.

Apache 2.0: see LICENSE. Material from other projects keeps its own licence. NOTICE and THIRD_PARTY.md list it, PUBLISHED-WORKS.md lists the published works that the code applies or names, and licenses/ has the texts.

We thank Alessandro Chiesa, Giacomo Fenzi, Guy Weissenberg, Miranda Christ, Rahul Dalal, and Ben Mayer for their input and collaboration on FlashProve. We also thank James Petrie for VerInf.