Proofs are cheap now. Specs are next

QuickProof, a tool that lets developers write formal specifications for C code as small C programs, turns those specs into Rocq theorems that AI agents then prove, with the Rocq proof checker verifying every step so nothing the agents write needs to be trusted. The tool addresses the specification bottleneck in formal verification: an agent that cannot find a proof may weaken the statement or add an assumption, and QuickProof's `qp verify` step rebuilds the proof from a fresh clone to confirm the statement is unchanged and uses only standard axioms. The post also demonstrates that the same process finds bugs, including in libraries that were already verified.

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 https://www.genproof.com/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 linux-a-two-decade-old-cve . 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: 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 https://vst.cs.princeton.edu/ , 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 https://www.genproof.com/quickproof/docs/check-a-proof 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 assume s satisfies all its qp assert s 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 dozens of 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 https://bugs.genproof.com/ where the code violates them. Linux: a two-decade-old CVE Theorem and Anthropic recently verified https://www.anthropic.com/research/formal-verification 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 https://github.com/redis/redis stores small hashes, lists and streams in listpacks , a compact format with its own format specification https://github.com/antirez/listpack . 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 https://github.com/redis/redis/issues/16078 . 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 https://github.com/meta/zstd , OpenSSL https://github.com/openssl/openssl , Mbed TLS https://github.com/Mbed-TLS/mbedtls , LZ4 https://github.com/lz4/lz4 , nginx https://github.com/nginx/nginx , c-ares https://github.com/c-ares/c-ares , nghttp2 https://github.com/nghttp2/nghttp2 , nanopb https://github.com/nanopb/nanopb , protobuf-c https://github.com/protobuf-c/protobuf-c , musl https://musl.libc.org/ 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 https://bugs.genproof.com/ . QuickProof vs. OSS-Verify Let's compare QuickProof with OSS-Verify, a recent project by Anthropic and Theorem. They announced https://www.anthropic.com/research/formal-verification 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: js 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 https://github.com/meta/zstd/issues/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 450,000 lines of Rocq, since it reasons about every instruction of the binary. Our zstd proof https://www.genproof.com/quickproof/proofs/zstd 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 https://github.com/genproof/quickproof-public . Write a spec for your own C library, let an agent prove it, and check the proof yourself with qp verify https://www.genproof.com/quickproof/docs/check-a-proof . We'd like to hear what you find.