Proofs are cheap now. Specs are next

For decades, proving that software is correct had two problems that kept most developers away: the specification had to be written in the language of a proof assistant such as Lean or Rocq (formerly Coq), and the proof was long, often many times longer than the code. The second problem is going away. AI agents now write formal proofs, and a proof checker verifies every step, so a wrong proof can't get through.

The first problem is still there, and agents make it more important. The proof checker guarantees that the stated theorem is proved, not that it is the theorem you meant. An agent that can't find a proof may weaken the statement or add an assumption, and if you can't read the statement, you can't tell.

QuickProof solves the first problem for C. It lets you write the specification in the language of the code itself: a small C program that calls your library, much like a test. QuickProof turns it into a theorem, AI agents prove it, and Rocq checks the proof. Nothing the agents write needs to be trusted.

This post shows how to state and prove properties of production C code with QuickProof. The same process finds bugs, even in libraries that are already verified.

Specs in C

Let's take the good old compression round-trip property: decompressing must give back what was compressed. In QuickProof, the spec is a C program:

int main(void) {
    uint8_t data[4096], packed[8192], unpacked[4096];
    size_t n = nondet_size();       // any length ...
    qp_assume(n <= sizeof data);    // ... up to 4 KiB
    nondet_bytes(data, n);          // any contents
    size_t m = compress(data, n, packed);
    size_t k = decompress(packed, m, unpacked);
    // decompressing gives back the original data
    qp_assert(k == n && memcmp(unpacked, data, n) == 0);
    return 0;
}

It reads like a property-based test, with three kinds of special functions:

  • nondet_* ("nondeterministic") gives an arbitrary input;
  • qp_assume restricts the inputs;
  • qp_assert checks a result.

A test checks the inputs it happens to try. A proof covers every input the spec allows: here, every byte string of up to 4 KiB.

Here is what QuickProof does with this spec:

The QuickProof pipeline: spec in C, qp assemble, AI agents, qp verify; the result is a theorem or a counterexample.

First, qp assemble turns the spec and your library into a theorem in the Rocq proof assistant: every qp_assert holds for every allowed input, and the code has no undefined behavior (more on that below). The theorem statement is fixed before any proof work starts.

Then AI agents prove it in the Verified Software Toolchain (VST), a Rocq framework for C. They write the function specifications of compress and decompress, their loop invariants and the proofs, and they may change only proof files. If decompress lost a byte on some input, the proof would get stuck, and the agent would look for that input: you would get a bug with a reproducer instead of a theorem.

Finally, qp verify rebuilds the proof from a fresh clone and checks two things: that the statement is unchanged, and that the proof uses only standard axioms. So an agent can't cheat by weakening the statement or by assuming what it has to prove.

How we translate specs to Rocq

The translation is simple, and this is what makes QuickProof trustworthy. We use VST, a Rocq framework for reasoning about C programs, developed at Princeton for over a decade and used, for example, to verify OpenSSL's SHA-256. For the spec's main, the only thing we state in VST is that it has no undefined behavior (in particular, it is memory-safe).

To the environment of the program we add exactly three specifications, one for each kind of special function. They are what turn "the property holds" into "no undefined behavior".

  • nondet_*: the specification says only that the result has the right type. The proof therefore has to work for every value, which is exactly "any input".
  • qp_assert(c): the specification requires c to hold before the call, so every assertion is something the proof must show.
  • qp_assume(c): the specification promises that c holds after the call.

So the theorem states that, whatever values the nondet_* calls return, each run of the spec that passes its qp_assumes satisfies all its qp_asserts and has no undefined behavior. This rules out memory errors (out-of-bounds accesses, use-after-free, double free, null dereferences, reads of uninitialized memory), division by zero, bad shifts and signed overflow, in your library as well as in the spec.

Nowhere for bugs to hide

We took 20 popular C projects and wrote specs for them. For some of them, we asked an AI to translate the promises made in the documentation into specs, and then reviewed the specs ourselves. That alone was enough: trying to prove these specs, we found more than 300 bugs where the code violates them.

Linux: a two-decade-old CVE

Theorem and Anthropic recently verified a core component of the Linux kernel and concluded that it is "almost fully correct", apart from a few minor, unexploitable bugs in corner cases. When we verified the same code, we found a flaw that has been there for two decades and can be exploited remotely to switch a device off. We have reported it as a CVE.

Redis: an upgrade that crashes the server

Redis stores small hashes, lists and streams in listpacks, a compact format with its own format specification. The format specification defines what a valid listpack is, and Redis promises to accept valid listpacks. So our spec says: every listpack that is valid by the format specification passes Redis's deep validation and reads back exactly.

int main(void) {
    struct model m;
    // any listpack, written by the rules of the listpack specification
    unsigned char *lp = write_any_listpack(&m);
    qp_assume(lp != NULL);
    // Redis's deep validation accepts it ...
    qp_assert(lpValidateIntegrity(lp, lpBytes(lp), 1, NULL, NULL) == 1);
    // ... and reading it gives back every entry that was written
    unsigned char *p = lpFirst(lp);
    for (size_t i = 0; i < m.n; i++) {
        qp_assert(entry_is(p, &m, i));
        p = lpNext(lp, p);
    }
    qp_assert(p == NULL);
    return 0;
}

write_any_listpack and entry_is come from a C model of the format specification, a few hundred lines written from its tables: the writer uses nondet_* to choose the entries and encodes them in every way the format specification allows.

On Redis 8.10, the proof of this spec got stuck. At three entry lengths (16,383, 2,097,151 and 268,435,455 bytes) the listpack format allows two encodings of the entry's length field. Redis up to 8.6 wrote the longer one. A fix in 8.8 switched to the shorter one, but the same function is also used to read existing entries. So Redis 8.8 and later misread entries written by 8.6 and earlier. With default settings, the first command that reads such an entry, say a stream field of 16,378 bytes, fails an assertion and stops the server. With full payload sanitization, the server refuses to load the RDB snapshot at all. Routine operations are enough to hit it: upgrading a server, upgrading a replica before its primary, restoring a dump. We reported it.

Why didn't tests or fuzzing catch it?

Tests build listpacks with Redis's own writer, so they only check that a version reads back what that same version writes, and that round trip works in 8.6 and in 8.8 alike. The bug only shows up for an entry written by one version and read by another. A fuzzer would have to produce the longer encoding at one of three specific lengths, and even the smallest of these entries, at almost 16 KiB, is larger than the inputs fuzzers usually generate. Our spec doesn't depend on any version of Redis: it takes every listpack the format specification allows, in every encoding. The proof can't skip the boundary lengths, so it got stuck at those three, and the counterexample showed the bug.

Not just Linux and Redis

The same approach found bugs in zstd, OpenSSL, Mbed TLS, LZ4, nginx, c-ares, nghttp2, nanopb, protobuf-c, musl and many other libraries, and in the Linux kernel. Each bug is real and comes with an input that triggers it, and some are serious. All the bugs, with their status upstream, are at bugs.genproof.com.

QuickProof vs. OSS-Verify

Let's compare QuickProof with OSS-Verify, a recent project by Anthropic and Theorem. They announced that Claude had verified 239 entry points of 123 open-source libraries. This is impressive work, and it shows that AI agents can now write formal proofs at a scale nobody could afford before. Unlike ours, their statements are about the compiled RISC-V binary, so the compiler doesn't have to be trusted.

We wanted to see what such a proof tells you about a library. So we took six of the libraries whose proved entry points are in the OSS-Verify public release: zstd, OpenSSL, libpcap, zlib, Mbed TLS and coturn. We wrote QuickProof specs for them and found bugs in all six.

This doesn't mean their proofs are wrong: they are machine-checked, and none of our bugs contradicts any of their proved statements. It means that their statements say little about what the library computes. The statements are derived automatically from the libraries' fuzz targets, which are written to find crashes, not to check results.

Let's look at zstd. Here is its zstd_frame_info fuzz target (abridged), one of those with proved statements:

int LLVMFuzzerTestOneInput(const uint8_t *src, size_t size) {
    ZSTD_FrameHeader zfh;
    ZSTD_getFrameContentSize(src, size);
    ZSTD_findFrameCompressedSize(src, size);
    ZSTD_getDictID_fromFrame(src, size);
    // ... six more functions
    ZSTD_getFrameHeader(&zfh, src, size);
    return 0;
}

It calls ten frame-inspection functions on arbitrary bytes and throws their results away. Its proof says that none of them crashes, and nothing about what they return. When we wrote QuickProof specs for the same functions, checking their results against what zstd.h documents, we found that ZSTD_getDictID_fromFrame returns the wrong value for skippable frames (zstd#4881): a bug in a function their proof covers, but one the proof can't see, because nothing looks at the result.

Our stronger spec doesn't need a bigger proof, either. Their proof for zstd_frame_info is about 600,000 lines of Rocq, since it reasons about every instruction of the binary. Our zstd proof is about the same size, and it proves much more: 19 properties of zstd's decoder, including the one about ZSTD_getDictID_fromFrame, with each function's proof shared by every property that uses it. Along the way, we found more than 20 bugs and cases of undefined behavior in zstd.

Try it!

You can try QuickProof here. Write a spec for your own C library, let an agent prove it, and check the proof yourself with qp verify. We'd like to hear what you find.

← Back to blog