QCP team releases the PV-BENCH program verification benchmark

AI is making it more efficient to write and modify programs, but establishing whether the generated code actually meets its requirements still calls for reliable checks. Testing can reveal errors; formal verification goes further by using precise specifications and mathematical proofs to establish that a program meets its requirements for every input satisfying its precondition.

Automating this work with AI remains difficult. Expressing requirements accurately, choosing loop invariants, and proving algorithmic properties together with memory correctness all require expertise. A shortage of high-quality training data is one constraint: publicly available code is abundant, but verification examples with complete specifications, annotations, and proofs remain relatively scarce.

Complete examples make the process of turning algorithmic concepts into specifications and proofs concrete. For sorting, an ordered result is only part of the requirement: the specification must also preserve the original elements and their multiplicities. C programs with different data structures or performance optimizations require further choices about describing memory, relating mathematical objects to concrete storage, and organizing proofs. These design choices and proof methods are precisely the experience that models need to learn and researchers seek to reuse.

To address this need, the QCP team has released PV-BENCH, a collection of 233 C program instances. The team incorporated its specification and proof experience into AI-agent workflows. Under expert supervision and review, the programs were specified and verified using QCP through automated agent work or human–AI collaboration.

PV-BENCH releases programs, specifications, annotations, and proofs together. These provide verification examples that researchers can study and reuse, as well as a basis for evaluating fully automated program verification, including methods that improve efficiency and reduce cost.

Explore PV-BENCH: Hugging Face dataset · GitHub repository

From classical algorithms to competition-level programs

This release of PV-BENCH draws from two main sources:

• 86 algorithm, data-structure, and engineering instances: 41 classical algorithm implementations, 13 LeetCode instances, 19 Luogu instances, five data-structure modules, and eight engineering routines, including C string and memory functions and dynamic vectors from MiniSat.
• 147 Codeforces instances: problem ratings range from 800 to 2800, with 26 rated at least 2000. Language models generated these C implementations from problem descriptions, and the implementations passed the corresponding online judge under its time and memory limits. They then became fixed inputs for verification evaluation.

The programs cover sorting, greedy algorithms, dynamic programming, graph algorithms, number theory, and computational geometry. Selected algorithms have multiple implementations, allowing researchers to examine how specifications and proofs accommodate different control flows and data layouts:

• Quicksort: five implementations of two partition schemes: Hoare partitioning, which scans inward from both ends of the array, and Lomuto partitioning, which scans in one direction from one end. The Hoare variants use swaps or vacant-position filling, with different treatments of recursion boundaries.
• Prim's minimum spanning tree algorithm: adjacency-matrix implementations returning either the tree's total weight or its adjacency matrix, and an implementation using forward-star adjacency arrays and a heap with decrease-key support, returning arrays of tree edges.
• Depth-first search (DFS): graph storage as a flat adjacency matrix, a two-dimensional adjacency matrix, or linked adjacency lists.

Each instance includes a problem statement, fixed C source code, an expert-reviewed reference specification, reference annotations, and complete verification artifacts. QCP discharges some verification conditions automatically, with supplementary Rocq proofs covering the remainder.

Evaluating specifications, annotations, and proofs separately

PV-BENCH defines three independent tasks, each targeting a key part of verification:

• Specification generation: write input conditions, output requirements, and supporting mathematical definitions from the problem statement and fixed code.
• Program annotation: given the code and reference specification, add loop invariants, intermediate assertions, and other annotations needed for verification.
• Proof completion: given the reference specification and annotations, prove in Rocq the verification conditions that QCP cannot discharge automatically.

The three tasks are evaluated independently, using reference artifacts wherever inputs from preceding stages are needed. For example, proof completion uses reference specifications and annotations directly, so errors in generating them do not propagate into the proof task. This helps identify which stage presents difficulties.

Evaluation checks both whether the generated artifacts pass verification tools and whether a generated specification expresses the same requirements as the reference. This prevents a weaker requirement from being mistaken for successful verification.

Representative examples: from program behavior to mathematics

These tasks require proofs of functional correctness, beyond memory safety alone. The following three examples illustrate the verification challenges posed by different programs.

Graph representations: different memory layouts, the same reachability requirement

The same graph can be stored as a flat adjacency matrix, a two-dimensional adjacency matrix, or linked adjacency lists. Below we compare DFS implementations using linked adjacency lists and a two-dimensional adjacency matrix. Both use vertex as the starting vertex and the visited array to record the result.

Linked adjacency lists. adjacency[u] points to the neighbor list for vertex u. Each node stores a neighbor's index and a pointer to the next node.

void dfs_adjacency_list(struct list **adjacency, int vertex_count,
                        int *visited, int vertex);

A two-dimensional adjacency matrix. matrix[u][v] is 1 if there is an edge from u to v, and 0 otherwise.

void dfs_adjacency_matrix_2Darray(int **matrix, int vertex_count,
                                  int *visited, int vertex);

Both implementations must establish that DFS visits every vertex reachable from the starting vertex. The details of their proofs, however, depend on different graph representations: the first uses adjacency lists, while the second uses an adjacency matrix.

This example shows how different implementations of the same algorithm can share a mathematical description of their functional requirements while needing their own memory descriptions. Program verification must connect abstract functional requirements to concrete data representations.

View the specifications and supporting definitions: linked adjacency lists · two-dimensional adjacency matrix

Dynamic vectors in MiniSat: how growth affects the element sequence

MiniSat is a small, open-source Boolean satisfiability (SAT) solver: it determines whether a Boolean formula has an assignment of variables that makes it true. PV-BENCH includes the definitions and implementations of dynamic vectors used in MiniSat. The following example focuses on its integer vector:

struct veci_t {
    int    size;
    int    cap;
    int*   ptr;
};
typedef struct veci_t veci;

size is the number of stored elements, cap is the number of elements the buffer can hold, and ptr points to that buffer. Only the first size positions belong to the current sequence; the rest are reserved space. The diagram shows what happens when an element is appended to a full buffer:

The following declaration is for the append function, veci_push(v, e). It adds e to the end of the vector, first growing the buffer if it is full.

void   veci_push   (veci* v, int e)
/*@ With (xs : list Z) (buf : Z) (cap : Z)
    Require
      ... && veci_raw(v, buf, cap, xs)
    Ensure
      exists buf2 cap2, ... &&
        veci_raw(v, buf2, cap2, app(xs, cons(e, nil)))
*/;

Verification must establish that every original element is preserved, with exactly one e appended. In the diagram, appending 50 to [10, 20, 30, 40] produces [10, 20, 30, 40, 50]. With spare capacity, the buffer address and capacity remain unchanged. A full buffer must grow and may move to a new address. On either execution path, the elements and their order must match the required append behavior.

This example shows how a simple append operation can involve growing capacity, relocating memory, and updating structure fields. Verification must establish that these operations together append an element to the sequence while keeping length, capacity, and buffer contents consistent. Yet the resulting specification is a simple description of the function's behavior, without the concrete details of the underlying storage. Storage details are hidden in the proof; the externally promised behavior should be expressed concisely.

View the structure, function specification, and supporting definitions

Inconvenient Pairs: from detours to counting pairs

Codeforces 1569D, Inconvenient Pairs, gives horizontal and vertical streets spanning a city, with people standing on those streets. Two people form an inconvenient pair if the shortest route between them along the streets is strictly longer than their Manhattan distance. The task is to count these unordered pairs, counting each pair once.

For example, suppose adjacent horizontal streets lie at y = 0 and y = 4, and two people stand on vertical streets at (0, 1) and (2, 2). Their Manhattan distance is 3, but they must reach a horizontal street to turn, making the shortest route 5. They therefore form an inconvenient pair.

Below is the declaration of the solving function, solver, which returns the number of inconvenient pairs. xs and ys store the x-coordinates of vertical streets and the y-coordinates of horizontal streets; px and py store each person's coordinates. The final four arrays provide workspace for grouping and sorting.

static long long solver(const int *xs, int n, const int *ys, int m,
                        const int *px, const int *py, int k,
                        int *va_grp, int *va_key,
                        int *ha_grp, int *ha_key);

The implementation counts pairs by identifying strips, sorting, and grouping. To show that this counting method meets the problem requirements, verification must first justify a geometric equivalence: inconvenient pairs occur exactly when both people lie strictly between the same two adjacent horizontal streets but on different vertical streets, or strictly between the same two adjacent vertical streets but on different horizontal streets. A person at an intersection cannot form an inconvenient pair. Each strip therefore contributes all pairs within it minus pairs on the same street.

Verification must establish both that the program performs the grouping, sorting, and counting correctly and that this counting method is equivalent to the shortest-path condition in the problem. The mathematics behind the problem is part of the correctness proof.

View the Inconvenient Pairs specification and supporting definitions

PV-BENCH makes this specification and proof experience available as public, checkable reference artifacts. Its three independent tasks—specification generation, program annotation, and proof completion—help researchers examine AI's capabilities and limitations in automated verification. We hope these examples will support research into future models and methods, provide a common basis for measuring progress, and advance more efficient, lower-cost fully automated program verification.