What is QuickProof

QuickProof proves properties of C code. You write each property as an executable spec, a small C program you can run. AI agents write a proof that it holds for every input the spec allows. Coq checks the proof, and anyone can check it again with qp verify.

• We proved C specs of zlib 1.3.2, WireGuard in Linux, OpenSSL's punycode decoder and zstd's decoder. False ones showed bugs in zlib and in the kernel.
• To start from tests you already have, qp import-fuzz turns a libFuzzer target into a spec: no input of any length makes it crash (Import fuzz targets). In v0.1 that import is stable. Its options for AFL++ and honggfuzz harnesses and for other entry points, and the importers for CBMC (Import CBMC harnesses) and SV-COMP (Import SV-COMP tasks), are previews. No property imported from CBMC or SV-COMP has been proved yet.

Example#

From examples/rle:

/* Law rle_decode_safe: for every input of up to 4 KiB, rle_decode never reports more output than the buffer it
   was given, and never reads or writes out of bounds. */
#include <stdlib.h>
#include "quickproof.h"
#include "rle.h"

int main(void) {
    size_t n = nondet_size();          /* any length ...    */
    qp_assume(n <= 4096);              /* ... up to 4 KiB   */
    uint8_t *in = malloc(n);
    if (in == NULL)
        return 0;
    nondet_bytes(in, n);               /* any bytes         */

    uint8_t out[256];
    size_t m = rle_decode(in, n, out, sizeof out);
    qp_assert(m <= sizeof out);

    free(in);
    return 0;
}

nondet_* is the input, qp_assume restricts it, and qp_assert checks the result. A spec is what qp and its reports call a law. QuickProof turns the spec, linked with the library, into Theorem rle_decode_safe : harness_safe whole_prog. Once proved, the claim in the first comment holds for every input of up to 4 KiB. This property is narrow: it bounds the length of the output but does not say what the output should be.

How it works#

1. Pin the code at an upstream commit, and patch idioms that CompCert leaves undefined or VST cannot handle, such as goto.
2. Write and review the specs.
3. qp check runs each spec natively under sanitizers, under CompCert's interpreter and against broken versions of the library. False properties usually fail here in seconds.
4. qp assemble generates the theorems and commits them, unproved, under the tag contract.
5. AI agents write the proof. For a false property they look for an input that breaks it (bugs found).
6. qp verify rebuilds the proof from a fresh clone, compares the theorems with the contract and checks the axioms (The qp command).

What you review#

Nothing AI agents write for the proof is trusted. You review the spec, which states the property, with its qp_assume lines, its quickproof.conf, any models of operating-system or kernel interfaces, and the limits of the proof. For zlib 1.3.2 the specs are about 5,500 lines against about 590,000 lines of proof.

Results#

Each repository's README says what its specs state, what the proof leaves out, and how to check it with your own QuickProof checkout. Each theorem is about the code its repository holds: an upstream commit with the edits and fixes listed there. Check times are those of qp verify on 16 CPUs.

Bugs found#

We report every bug to its maintainers before we publish anything about it, so this list lags behind the work.

• Linux lib/crypto: Poly1305 and ChaCha20-Poly1305 went wrong for lengths of 4 GiB and more; no caller in the kernel passes such lengths. Eric Biggers' series fixes it and credits our report.
• zlib: #1300, fixed by #1326; #1348, fixed in 2bed3d61; #1297, merged as 066e0b68; #1283, closed without a change; four reported by e-mail, fixed upstream in e7bb9788, 8179479c and c0424159, or documented in dfa96642.
• XZ Utils: #237, closed: the maintainer considers NULL + 0 fine, since C2y defines it.

Limitations#

QuickProof 0.1 is a research preview. The tool, its file formats and its documentation will change.

• The theorem is about the C source as CompCert defines C, on 64-bit x86. The compiler and the system's libc are not covered. Undefined behaviour is what CompCert's semantics leaves undefined, plus VST's checks. That is stricter than ISO C in some places and more permissive in others (What a proof means).
• It answers only the question the spec asks.
• It is partial correctness: a run that never returns is not a failure. Memory leaks and running out of stack are not ruled out either.
• It covers runs of one thread. Assembly, SIMD intrinsics and most floating-point code are out of reach.
• Idiom patches and models of operating-system or kernel interfaces are tested, not proved. Each proof repository lists them: WireGuard in DEVIATIONS.md, zlib and OpenSSL in patch/PATCH.md, zstd in patch/GENPROOF-PATCH.md.
• VST's adequacy theorem, from the theorem to "no run has undefined behaviour", is not yet instantiated in Coq for QuickProof's environment; that instance is upcoming. Every theorem so far rests on 13 or 14 axioms, standard logical ones and the declarations of VST's abstract malloc library.
• Coq, VST, CompCert's semantics of C, clightgen, QuickProof's translation scripts, its model of the environment (include/quickproof.h, coq/QuickProof/Env.v, coq/QuickProof/Contract.v) and qp verify are trusted.

License#

QuickProof is under the PolyForm Noncommercial License 1.0.0 (LICENSE), copyright 2026 GenProof. It is built on the Verified Software Toolchain (Andrew Appel and colleagues at Princeton), CompCert (Xavier Leroy and colleagues at Inria) and Coq.

The toolchain it uses, which the Docker image ships, includes CompCert under the INRIA Non-Commercial License. That licence allows educational, research and evaluation use; commercial use of CompCert needs a licence from AbsInt. Coq is under the LGPL 2.1, and VST under a BSD licence.

We chose a noncommercial license to make QuickProof freely available for community use while reflecting CompCert’s licensing restrictions. We remind users that commercial use of CompCert requires separate permission.

Required Notice: Copyright 2026 GenProof (https://genproof.com)