---
title: GenProof's QuickProof lets you write C specs like tests and has AI agents prove them in Rocq; it reports 300+ bugs in 20 projects, including six libraries covered by Anthropic and Theorem's OSS-Verify | ctxsec
url: https://ctxsec.com/items/genproof-quickproof-specs-in-c-300-bugs-redis-listpack-upgrade-crash-oss-verify-libs
description: "GenProof released QuickProof: you write a specification as a small C program (arbitrary inputs, assumptions, assertions), it becomes a Rocq/VST theorem, AI agents write the proof and a checker verifies it, rejecting any proof that weakens the statement. GenProof says doing this for 20 popular C projects found more than 300 spec violations, including a Redis bug where 8.8+ misreads listpack entries written by 8.6 and earlier and can crash on upgrade, and a two-decade-old remotely triggerable Linux flaw it has reported for a CVE."
status: "official (GenProof launch post, Nov 2, and public bug tracker). Vendor research; bug counts are GenProof's own"
published: 2026-11-03
---

> GenProof released QuickProof: you write a specification as a small C program (arbitrary inputs, assumptions, assertions), it becomes a Rocq/VST theorem, AI agents write the proof and a checker verifies it, rejecting any proof that weakens the statement. GenProof says doing this for 20 popular C projects found more than 300 spec violations, including a Redis bug where 8.8+ misreads listpack entries written by 8.6 and earlier and can crash on upgrade, and a two-decade-old remotely triggerable Linux flaw it has reported for a CVE.

[← AI](/ai) · [markdown](/items/genproof-quickproof-specs-in-c-300-bugs-redis-listpack-upgrade-crash-oss-verify-libs.md)

official (GenProof launch post, Nov 2, and public bug tracker). Vendor research; bug counts are GenProof's own

2026-11-03

### GenProof's QuickProof lets you write C specs like tests and has AI agents prove them in Rocq; it reports 300+ bugs in 20 projects, including six libraries covered by Anthropic and Theorem's OSS-Verify

GenProof also wrote specs for six libraries in the OSS-Verify release (zstd, OpenSSL, libpcap, zlib, Mbed TLS, coturn) and found bugs in all six. It stresses that this does not make those proofs wrong: they were derived from fuzz targets and prove the code doesn't crash, not that results are correct. Its example is `ZSTD_getDictID_fromFrame` returning the wrong value for skippable frames (zstd#4881).

**Takeaway for security teams:** 'formally verified' is only as strong as the statement that was proved. When a vendor or project cites a proof, ask what property it covers (no crashes, memory safety, functional correctness) before treating it as a security guarantee. Bugs and their upstream status are listed on GenProof's tracker.

Sources: [GenProof: Proofs are cheap now. Specs are next (Nov 2)](https://www.genproof.com/blog/quickproof) · [GenProof bug tracker](https://bugs.genproof.com/) · [Anthropic: LLMs are making formal software verification feasible at a much larger scale](https://www.anthropic.com/research/formal-verification)