Comparison

QuickProof proves properties of existing C code for all inputs up to the bounds the property states. Each property is a C program, a harness. AI agents write a Rocq (formerly Coq) proof in VST, the Verified Software Toolchain, against CompCert's semantics of C, and Rocq checks it.

Fuzzers (libFuzzer, AFL++, honggfuzz, OSS-Fuzz)#

A fuzzer is cheap to start, finds real bugs quickly and needs no proof. It only checks the inputs it tries, so inputs it rarely builds, such as very long ones, stay untested. A QuickProof harness looks much like a fuzz target, and its proof covers every input the harness allows. qp import-fuzz turns a libFuzzer target into a harness, and qp fuzz --libfuzzer runs a harness as one, so a false property usually shows a counterexample before anyone works on a proof.

Bounded model checkers (CBMC, ESBMC, Kani)#

CBMC and ESBMC translate a C program, with loops unrolled to a chosen bound, into a formula for a SAT or SMT solver; Kani does the same for Rust. They need no proof from the user and give a concrete trace for each failure. Their results hold for the input sizes and loop bounds the harness sets; CBMC's unwinding assertions check that the bound suffices for those inputs, and ESBMC can prove some properties without a bound, by k-induction. The model checker and the solver are trusted. QuickProof's theorems have no bound beyond the harness's, and Rocq's kernel checks them. qp import-cbmc takes CBMC proof harnesses as they are, so the two can be compared on the same claim.

Deductive verifiers for C (Frama-C/WP, VeriFast)#

Frama-C's WP plug-in proves C functions against contracts written in ACSL annotations. It generates proof obligations and sends them to automatic provers, or to Rocq for the hard ones. VeriFast verifies C (and Java and Rust) annotated with separation-logic specifications, by symbolic execution. Both are mature and have verified real code. In both, the specifications are written into or next to the source. The verifier is trusted, and for WP so are the provers. In QuickProof the property is a separate C program, the agents write the function specifications in Rocq, and Rocq's kernel checks the proof against CompCert's semantics.

Proof assistants (RefinedC, VST, AutoCorres, seL4)#

RefinedC proves C code against refinement types written as annotations, largely automatically, and Rocq checks the result, built on Iris and RefinedC's own semantics of C. QuickProof builds on VST, which is proved sound in Rocq against CompCert's semantics, and adds the translation of a harness into a VST theorem, the checks around it, and qp verify.

The seL4 microkernel was proved correct in Isabelle/HOL, from an abstract specification down to its C code and, by translation validation, the compiled binary, in many person-years of expert work. A C parser translates its C into Isabelle, and AutoCorres, from the same group, turns such translations into functions that are easier to reason about. QuickProof's results are much narrower: properties stated by harnesses, about the source code only, with partial correctness and one thread.

New verified code (HACL*, Low*, fiat-crypto)#

HACL* is cryptographic code written and verified in F* (its Low* subset) and compiled to C. fiat-crypto generates C for field arithmetic from proved Rocq definitions. Both produce new code with full functional correctness. QuickProof starts from C code that is already in use, and proves the properties that the harnesses state.

AI agents and Lean (Certora's zlib proof, lean-zip)#

In September 2026 Certora published a proof, written by LLMs in Lean 4, that zlib 1.3.2's inflate_table is memory safe, terminates and writes only the memory it should. The proof uses CLean, a fork of CompCert's clightgen that emits Lean, and a Lean version of CompCert's semantics of Clight, the C dialect that clightgen produces, tested against CompCert. It covers termination, which ours does not, uses unmodified code and rechecks in seconds. Our zlib proof covers the core library, inflate_table included as inflate calls it. It states functional properties, such as exact round trips, bounded memory and safe decompression of any input. It builds on VST's soundness proof against CompCert's own semantics, and it is about the code with edits for the tools, tested, not proved, and fixes for the bugs it found.

lean-zip is a zlib reimplemented in Lean by AI agents, with a theorem that decompression undoes compression. Like HACL*, it is new code written to be verified, and it proves nothing about the existing C zlib.

When to use something else#

• Termination and total correctness (Certora's zlib proof; Frama-C/WP with loop variants).
• Proofs about the compiled binary (seL4).
• Fully automatic checking without a proof (fuzzers, CBMC, ESBMC, Kani).
• Fast rechecks. A QuickProof proof is long, and its check takes from a minute for a small example to many hours for a large proof.