PV-Bench: Specification and Verification of Competition-Level Algorithmic Programs

Automating the verification of existing code requires both formalizing its intended behavior and proving that the implementation satisfies it. Many existing benchmarks let models generate the implementations they verify, while fixed-program benchmarks often supply the specifications. We present PV-Bench, a benchmark for specifying and verifying fixed C programs that require reasoning about both algorithms and explicit memory manipulation. It contains 233 programs, including 147 accepted Codeforces solutions to problems rated from 800 to 2800, alongside classic algorithms, data structures, and library routines. Each program comes with an expert-reviewed reference specification and reference verification artifacts built with QCP. PV-Bench evaluates three tasks independently: specification generation, annotation generation, and completion of residual Rocq proofs. The latter two tasks receive the reference artifacts from preceding stages, allowing each capability to be assessed separately. Candidate specifications are checked for semantic equivalence to the reference through machine-checked proofs and refutations, distinguishing equivalent, too-weak, too-strong, and incomparable contracts while leaving unresolved judgments undecided. Annotation and proof submissions are checked against the fixed program and specification. Our evaluation reveals complementary strengths across stages and substantial gaps in specification and annotation generation, even when proof completion with reference specifications and annotations succeeds. These findings show why proof completion alone gives an incomplete picture of a model's ability to verify an existing program.