ULPBench: Autonomous Formal Verification of Numeric C

Machine-checked verification of critical C code, from cryptographic routines in OpenSSL to the seL4 microkernel, has historically demanded months to years of expert effort per component. Large language models (LLMs) are now capable of reasoning about C code and producing proofs in proof assistants such as Lean and Rocq, however these capabilities have largely been demonstrated for isolated pieces of the verification pipeline, such as synthesizing assertions or proving verification conditions, rather than for true end-to-end verification. In this paper, we explore the degree to which autonomous agents can perform end-to-end formal verification for numeric C code. To facilitate this, we introduce ULPBench, our custom verification benchmark consisting of 560 tasks drawn from production numeric C code. For each task, an agent is given a formal C semantics inside a proof assistant and must (i) write an executable functional model, (ii) prove that the C source refines it under that semantics, and (iii) prove a property of the model, such as a bound on floating-point error in terms of unit in last place (ulp). Completing all three stages of a task results in a full end-to-end proof, and each task is provided in both Lean and Rocq. To support the Lean side, we release a port of the CompCert Clight semantics and IEEE-754 binary32/binary64 floating-point semantics to Lean, providing the foundation needed to verify each real-world C program. We evaluate frontier agents, measuring success in end-to-end formal verification, and show that agents are able to autonomously formally verify challenging properties of C code in 36% of our test cases. Finally, we present a case study showing the use of this approach in practice which led to uncovering an unreported defect in CPython's atanh function as well as a defect in a major geospatial algorithm library.