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) · GenProof bug tracker · Anthropic: LLMs are making formal software verification feasible at a much larger scale