Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation
Organizations: Argonne National Laboratory, Lemont, Illinois, USA · University of Delaware, Newark, Delaware, USA
Abstract
Parallel numerical libraries such as PETSc are widely used in science and engineering applications where wrong results can have costly consequences. Despite this, numerical libraries are rarely formally verified. One of the challenges is the need for an expert to hand-write a specification and manually apply a verification tool, often requiring the development of a harness or driver, all of which can contain additional bugs that lead to false positives or false negatives during verification. With recent advancements in large language models (LLMs), it is tempting to generate such drivers and reference models automatically, but one-shot generation based on a simple prompt is brittle and leads to additional unverified code that needs to be audited. In this paper, we present an approach to use LLMs in a limited setting to generate a small, human-certifiable ACSL contract from the function's documentation, combined with a deterministic toolchain that supports a restricted ACSL profile and generates a driver that uses the CIVL verifier to check the implementation against the contract and, when available, an existing reference model. We demonstrate the pipeline end-to-end on three PETSc functions: MatAXPY (reference model already exists), MatAYPX (no reference model, so the certified contract is the sole oracle), and the non-compressing mode of MatFilter (no reference model, with more complex, conditional behavior). With this pipeline, we were able to discover a bug in PETSc's MatAYPX function that was previously undiscovered and had been present in the code since 1997.
Figures & tables
| Symbol | Stipulated meaning in the PETSc model |
|---|---|
| valid_mat ( M ) | is a matrix handle whose modeled dimensions, communicator, assembly state, and dense global image are consistent. |
| valid_vec ( v ) | is a vector handle whose modeled size, communicator, assembly state, and dense global image are consistent. |
| separated_mat ( A , B ) | and are distinct matrix objects with disjoint modeled storage. |
| separated_vec ( x , y ) | and are distinct vector objects with disjoint modeled storage. |
| same_comm ( x , y ) | The modeled PETSc objects use the same MPI communicator. |
| assembled ( x ) | The modeled object has no pending assembly updates. |
| Contract construct | Generated driver behavior |
|---|---|
| Supported requires equality | constrains symbolic dimensions or parameter values during driver construction. |
| Custom PETSc predicate | emits corresponding CIVL assumptions, construction constraints, or generated cases. |
| assigns over modeled data | records pre-call values outside the assignable set and checks that those values remain unchanged after the call. |
| Supported ensures | translated into elementwise CIVL assertions over the gathered global image; \ old terms refer to recorded pre-call values. |
| Function | Case | str | Time (s) | Mem. (GiB) | States | Trans. |
|---|---|---|---|---|---|---|
| MatAXPY | aliased | D | 27.01 | 2.27 | 79,599 | 162,530 |
| MatAXPY | aliased | U | 29.09 | 2.36 | 79,599 | 162,530 |
| MatAXPY | distinct | D | 36.73 | 2.27 | 102,082 | 206,215 |
| MatAXPY | distinct | U | 34.36 | 2.27 | 102,082 | 206,215 |
| MatAYPX | aliased † | D | 6.75 | 1.30 | 1,615 | 3,460 |
| MatAYPX | aliased † | U | 7.06 | 1.71 | 1,615 | 3,460 |
| Function | PETSc body | Port | Drivers | Contract |
|---|---|---|---|---|
| MatAXPY | 39 | 23 | 176 | 14 |
| MatAYPX | 4 | 4 | 152 | 13 |
| MatFilter | 72 | 24 | 38 | 8 |
Formal Verification
Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.
See all 345 papers