Browse documentation

Check a proof

On this page

A QuickProof result counts only when qp verify accepts it. AI agents write the proofs, nothing they write is trusted, and anyone can run the check.

In Docker

The image contains Coq 8.20.1, CompCert 3.15, VST 2.15, QuickProof and its examples. The check takes a minute or two:

shell
docker run --rm ghcr.io/genproof/quickproof verify rle

With the toolchain installed

With the toolchain from Install, from a clone of QuickProof:

shell
git clone https://github.com/genproof/quickproof-public.git quickproof && cd quickproof
tools/qp examples rle      # one example
tools/qp examples          # all three

For each example, qp examples commits the example's code to a scratch git repository that stands in for an upstream. It runs qp assemble to generate the theorem and commit it unproved under the tag contract, commits the example's proof on top, and runs qp verify on the result. It needs no network. Examples describes the three examples.

A published proof

A proof repository is checked the same way, with a QuickProof checkout of your own at the release the proof pins, v0.1.0. For the zlib proof:

shell
git clone --branch v0.1.0 https://github.com/genproof/quickproof-public.git quickproof
git clone --recursive https://github.com/genproof/zlib-full-auto-proofs-public.git
quickproof/tools/qp verify zlib-full-auto-proofs-public --base contract

qp verify then checks that the framework inside the proof repository is, in every file that decides what a theorem says, the one you trust. Running the qp inside the proof repository would compare that copy with itself. Each proof repository's README gives its own command, with its contract tag after --base. Our runs took 17 minutes for OpenSSL's punycode decoder and about 7 hours for zstd's decoder with 8 build jobs, and about 19 hours for WireGuard with 4, on 16 CPUs.

Reading the report

This is the report of qp examples rle, from a real run (paths shortened):

# Verification of ~/.cache/quickproof/examples/rle/rle at 719039d0777f

- date: 2026-11-02 19:38
- framework: quickproof/ at fab76ef826ae (release v0.1.0)
- framework trusted files (16: the statement, the libc, the translation chain): identical to this verifier
- contract commit: ee20f552a920 (`contract`)
- files changed since the contract: 2; frozen files changed: none
- regenerated code.v: identical to the committed files
- elaborated statement and whole_prog of `rle_decode_safe`: identical to the contract
- `Admitted`/`admit`/`Axiom`/`Parameter`/`Conjecture` in the Coq sources of the proof (...): none

| theorem | result | axioms |
|---|---|---|
| `rle_decode_safe` | PROVED | 13: standard + VST malloc |

Verdict: PASS (exit 0).
  • framework trusted files. The files that define what a theorem says and how C becomes Clight, the C dialect that CompCert and VST work with, are byte for byte those of the verifier you run. They are quickproof.h, the Rocq library coq/QuickProof/, the plain-C libc and the translation scripts. A proof repository cannot bring a weaker framework.
  • files changed since the contract. The commit tagged contract holds the specs, the code and the generated theorems, before any proof work. Since then only proof sources and notes may change. Here the two files are src/proof/Decode.v, the specification and proof of rle_decode, and the contract file, where the proof of the theorem replaces Admitted.
  • regenerated code.v. The C code, translated to Clight again, must equal the committed Clight that the proof is about.
  • elaborated statement. Each theorem, as Rocq elaborates it, and a hash of the program it is about must equal the same theorem at the contract commit, regenerated from the spec. A proof of a different statement, or of a different program, fails here.
  • Admitted, admit, Axiom. None may appear in the proof's sources, even in a lemma that no theorem uses.
  • axioms. Print Assumptions of each theorem may name only standard logical axioms and VST's abstract malloc library. The 13 here are classical logic, functional and propositional extensionality, eq_rect_eq, proof irrelevance, extensionality of ensembles, two axioms of Rocq's classical reals, and five from VST's abstract malloc library: the declarations mem_mgr and malloc_token and facts about them, such as create_mem_mgr. The full list for each theorem is in VERIFY.md in the clone, and the accepted list is ALLOWED_AXIOMS in tools/qp.

A theorem that is still Admitted, or that depends on an Admitted lemma, shows up as not proved, and the verdict is FAIL. Your first property shows such a report.

What a PASS does not tell you

Whether a property asks the right question is for people to judge, by reading the specs. The first comment of each states its property in words, and the code below it is the claim. Then read the project's list of changes to the code and of the models of operating-system interfaces that it links (DEVIATIONS.md in WireGuard's repository, patch/PATCH.md in zlib's and OpenSSL's). Quote a result with both. What a proof means lists everything a result relies on.

Options

--coqchk also runs Rocq's independent checker, coqchk, on every module of the proof and of the framework's Rocq library. --base COMMIT names the contract commit when the clone has no contract tag; without one the result is UNVERIFIED, never PASS. -v prints every theorem's full Print Assumptions. The qp command describes every step of qp verify.