cert-machine · an outside check, November 2026

FlashProve, checked from the public bytes

FlashProve (Anthropic, released 30 October 2026 as a research artefact) lets a model provider prove that a reply came from the model it committed to, with a soundness theorem in Lean 4. Here a second party ran its verifier, its Lean library and its GPU route from the public repository at 9e2bdd8f, read its statements against what its theorems cover, and recomputed its numbers exactly. No tampered proof was accepted. The gaps below are already in FlashProve's own ledger; they sit between the README's sentences and that ledger.

steps certified

of 21 pre-registered

refused or not run

resources, a platform crash, and one error of ours

tampered inputs accepted

none: no tampered input accepted by either verifier, no suite row with status 3

gaps both readers found

each already stated in the claimant's ledger

§1 · the gaps

What the headline sentences leave out

Two readers read the README, the theorem file, the limits and gaps ledgers and the paper, each without seeing the other's table. A gap counts only if both found it. Every one is dated at the pin, 9e2bdd8f, and every one is already stated somewhere in FlashProve's own ledger; the column on the right says where.

	gap	where the claimant states it
G1	Nothing is proved about the programs a user runs. Soundness is a theorem about the Lean verify under a random oracle. It is not about cp_verify, and the hash is not BLAKE2b. README.md:15-16 tells users to check with cp_verify, next to the bound.	LIMITS L1, L4, L8; GAPS 45, 51; THEOREM.md:199-201
G2	"The committed model" means the weights an extractor reads. No theorem ties them to the provider's model or to cp_commit. No theorem ties a commitment ID to one set of public files, so one ID could pass with two file sets and two sets of weights.	LIMITS L2, L28; GAPS 64, 69, 77; THEOREM.md item 4
G3	The bound "q/2^124 + 2^-101" holds under conditions the README sentence does not give. It holds only at exact match, which verify does not test, while serving uses the clipped-gap policy. It holds only for files fixed before the hash is drawn, and it is the probability that one proof is both accepted and wrong. N proofs at once cost N times; proofs checked one after another have no bound.	LIMITS L4, L5; GAPS 5, 6, 44, 70; THEOREM.md:86, :300-303
G4	No real deployment is shown to satisfy the theorems. Completeness and zero knowledge hold for the Lean prover, on requests in CanServe. They are known to have content at one Lean value, storedSetup, whose scale file comes from synthetic weights. No proof on real weights has gone to the Lean verifier, and there is no theorem about the GPU prover.	THEOREM.md:41-44; GAPS 14, 52, 57; LIMITS L27, L69
G5	Weight hiding is proved only of the Lean prover, and it counts something else. The zero-knowledge count of 688,127 is single-request replies on one copy of the table. The programs stop a copy at 688,127 batches of up to 64 requests, and no theorem ties the two counts. The proof assumes fresh randomness, while the programs derive masks from a seed. The paper calls hiding by the programs "our judgement, not a proof".	LIMITS L83, L84, L93; GAPS 15, 15(3); paper abstract

One point a single reader raised was confirmed against the text: the small example that route 1 verifies is outside every theorem (THEOREM.md: "The small example's files are out of scope: verify rejects them"). A YES on it is a fact about the C++ program, not an instance of the soundness theorem. The merged reading is corpus/flashprove/readings/merged.md.

§2 · not decided

What this check did not settle

run_suite.py cpu (the claimant's own suite, CPU rows). REFUSED expected exit 0. One row of 92 (the Lean verifier's test script: 1 of 344 calls not as expected) failed, and our workflow did not keep that row's screen, so what the call was cannot be read from our facts: not decided either way. No row reported a false acceptance (status 3). (step R3, §3.1)
lake build of the library (default targets). REFUSED exit 139 is a segmentation fault of Lake itself at 37,583 of 37,650 jobs, every module before it built with the three standard axioms: a platform failure, not a failure of the claim. A re-run with fewer threads waits on CPU stock. (step L2, §3.2)
#print axioms of the six theorems from our own file. REFUSED not reached: the six theorems' module was among the 67 jobs L2 did not build (step L3, §3.2)
nanoda on exports of the six theorems. REFUSED not reached: their module was not built (L2) (step L5.six, §3.2)
our own byte-level parse of the proof header from docs/format/FORMAT.md. NOT RUN not written in this round; the differential of the two verifiers (L4) stands on one proof (step E3, §3.4)
the fresh GPU proof re-checked, and a tampered copy. NOT RUN OUR ERROR: our script passed the wrong paths for the config and key files, so neither check reached the proof. The proof itself was deleted with the pod. The GPU line above (the route's own cp_verify YES) stands; the second check does not exist. (step GPU.recheck, §3.5)

§3.1 · phase 1

Routes 1 and 2 on a hosted runner

step	what	word	what came back
pins	every pinned byte of the claim against corpus/flashprove/PINS.json	CERTIFIED	ok 80 files and the tree equal corpus/flashprove/PINS.json the clone re-hashed before any step
R1.1	verifier/build.sh builds cp_verify	CERTIFIED	exit 0; THE VERIFIER IS BUILT: /home/runner/fp/bin/cp_verify expected exit 0 and the BUILT line
R1.2	cp_verify on examples/accepted-proof (the small example)	CERTIFIED	exit 0; YES expected YES; the small example is outside every theorem (THEOREM.md:303), so this is a fact about the C++ program only
R1.3	cp_verify on examples/full-size	CERTIFIED	exit 0; YES; bits=128; proof of work: up to 32 bits counted in 71 rounds; with it the least round has 128.00 bits, without it 96.23 bits expected YES and bits=128
R1.4	six tampered inputs to cp_verify (a byte of the proof, the ID, the reply, a byte of the request, the proof cut by a byte, the wrong ID)	CERTIFIED	(a) exit 1 NO: proof-refused; (b) exit 1 NO: model-statement; (c) exit 1 NO: reply-differs; (d) exit 1 NO: statement-range; (e) exit 1 NO: proof-refused; (f) exit 1 NO: model-statement each must not be accepted; an exit 0 on any would be a finding
R2	blocks/first_look.sh (an honest copy accepted, a one-bit flip rejected)	CERTIFIED	exit 0 expected exit 0 and AS EXPECTED
R3	run_suite.py cpu (the claimant's own suite, CPU rows)	REFUSED	exit 1; run_suite.py: 90 rows passed, 1 passed in part (status 77: their last lines say what was not run), 1 failed, 0 not run, 0 left out under version word H821, 13 left out in mode cpu because they need nvcc or a GPU, 0 taken and not run (--taken) and 0 that only these need; failed: FAILED tools.lean_verify.script 153.7 s status 1; lean_verify_test.sh: 344 calls: NOT AS EXPECTED: 1; no row ended with status 3 (no false acceptance) expected exit 0. One row of 92 (the Lean verifier's test script: 1 of 344 calls not as expected) failed, and our workflow did not keep that row's screen, so what the call was cannot be read from our facts: not decided either way. No row reported a false acceptance (status 3).

§3.2 · phase 2

The Lean library on a CPU pod

step	what	word	what came back
L1	elan, Lean v4.29.1, Mathlib's cache, the pins	CERTIFIED	exit 0; Lean (version 4.29.1, x86_64-unknown-linux-gnu, commit f72c35b3f637c8c6571d353742168ab66cc22c00, Release)
L2	lake build of the library (default targets)	REFUSED	exit 139 after 21242 s; the last line built: [37583/37650] Built ShapeLines.Layers.Link22MembersOneToThree exit 139 is a segmentation fault of Lake itself at 37,583 of 37,650 jobs, every module before it built with the three standard axioms: a platform failure, not a failure of the claim. A re-run with fewer threads waits on CPU stock.
L3	#print axioms of the six theorems from our own file	REFUSED	exit 1; object file '/home/tester/fp/lean/.lake/build/lib/lean/AtFullSide/Face/TheSixLines.olean' of module AtFullSide.Face.TheSixLines does not exist not reached: the six theorems' module was among the 67 jobs L2 did not build
L4.cp	cp_verify built on the pod, on examples/full-size	CERTIFIED	exit 0; YES
L4.lean	the Lean verifier (tools/lean-verify) on examples/full-size	CERTIFIED	exit 0 after 1604 s; VERDICT: ACCEPT (exact match) expected ACCEPT, beside cp_verify's YES
L4.tamper	both verifiers on the full-size proof with its middle byte flipped	CERTIFIED	cp_verify exit 1 NO: proof-refused; the Lean verifier exit 2 NO VERDICT neither accepted it. The Lean verifier gave NO VERDICT, not the REJECT the pre-registration expected: its parser, outside Lean, refused the file, so Lean's own rejection path was not reached by this control.
L5.nanoda	nanoda (second kernel) on a PUBLIC lean4export of VerifierAndGoals.AtTheName.sound_of_verify_at — the route the claim's CHECKING.md calls "untried"	CERTIFIED	exit 0 after 860 s; 207,461 declarations checked, no typechecker error the three standard axioms permitted; the one pretty-printer error is nanoda's printer, not a check
L5.six	nanoda on exports of the six theorems	REFUSED	sound export exit 1; soundAndBinding export exit 1; completeOnCanServe export exit 1; zeroKnowledgeOnCanServe export exit 1; refusedHandsOutNoProof export exit 1; repliesFit export exit 1 not reached: their module was not built (L2)

§3.3 · phase 3

The statement reading

step	what	word	what came back
P3	two blind statement readings, merged (corpus/flashprove/readings/)	CERTIFIED	5 gaps found by both readers; each already stated in the claimant's own ledger a reading, not a proof: the word says the pre-registered procedure ran and gave its table

§3.4 · phase 4

Exact checks of our own

step	what	word	what came back
E1	the printed bounds against their Lean definitions, in exact rationals	CERTIFIED	soundness 2^-101 at q = 0, reaches 2^-40 at q = 19342813113833998067433472 (about 2^84); binding 2^-100 at q = 0; the exact values lie just above the printed "about" forms, by a factor 1 to six places "about q/2^124 + 2^-101" and "about q/2^124 + 2^-100" match finalSoundnessError and finalBindingError
E2	the field and the counts the statements name	CERTIFIED	p = 2^64 - 2^32 + 1 prime by a Pratt certificate checked here (two planted certificates refused); x^3 - 7 irreducible over F_p; p^3 < 2^192 (which the claim says it does not prove); 62 + 688,127·64 = 44,040,190 ≤ 44,040,191
E3	our own byte-level parse of the proof header from docs/format/FORMAT.md	NOT RUN	— not written in this round; the differential of the two verifiers (L4) stands on one proof

§3.5 · phase 5

Route 3 on one GPU

step	what	word	what came back
GPU	examples/quickstart-gpu.sh on one H100 (build, commit, prove a 64-token request, verify)	CERTIFIED	exit 0 after 1250 s; cp_verify YES; 3 "Compiled by" lines, each nvcc 13.2 V13.2.86
GPU.recheck	the fresh GPU proof re-checked, and a tampered copy	NOT RUN	cp_verify exit 2 on both: "input-unreadable-policy: policy.txt cannot be read: No such file or directory" OUR ERROR: our script passed the wrong paths for the config and key files, so neither check reached the proof. The proof itself was deleted with the pod. The GPU line above (the route's own cp_verify YES) stands; the second check does not exist.

§4 · limits

What this check is, and is not

Not a review of the cryptography. The theorems were checked to compile and, where the build finished, to rest on the standard axioms; their mathematics is the kernels', not ours. Nothing here is a security assessment.
Route 4 untouched. The 400B prover on real model weights was out of scope; no claim about it is decided here.
Pre-registered. Every step and its expected result were written and pushed before any run (notes/flashprove-preregistration-2026-11-04.md). No step was re-run to change its outcome.
Spend. Route 1: GitHub-hosted runner (free). Lean pod: ≈ US$12 (cpu3m 32 vCPU, about 6.9 h). GPU pod: ≈ US$1.81 (H100, 21 min).
Our own error, recorded. The second check of the fresh GPU proof did not run because our script passed wrong file paths; the proof was deleted with the pod. It is listed as NOT RUN, not as anything the claim did.

The record is certs/flashprove-check.json; the facts behind it are under corpus/flashprove/runs/.