PaperlayerView exact revision on arXiv

Source-linked AI summary

Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation

Hansol Suh, Jan Hückelheim, Stephen Siegel

arXiv:2609.31687v1cs.CLcs.MScs.PLcs.SE

TL;DR

PETSc is widely used in high-consequence applications, but extensive testing can miss subtle bugs, and unverified LLM-generated drivers are difficult to audit. The paper combines LLM-drafted, human-certified contracts with deterministic CIVL driver generation. Applied to three PETSc operations, the pipeline exposed a MatAYPX aliasing bug present since 1997.

  • Problem

    Extensive PETSc testing can miss subtle defects, while manually written verification artifacts are difficult to scale and one-shot LLM-generated drivers remain unverified code.

    Source: §I · p. 1

  • Method

    An LLM drafts a restricted ACSL contract from documentation, a PETSc-aware expert certifies it, and a deterministic compiler generates CIVL drivers.

    Source: §II · p. 3, B. Stage 1: from documentation to a… · p. 3, §VI · p. 8

  • Results

    The pipeline exposed a MatAYPX aliasing bug present since 1997: identical operand handles produce 2aY rather than (1 + a)Y.

    Source: §VI · p. 8

  • Takeaways & Limitations

    The pipeline confines direct review of LLM output to a compact contract and rejects constructs outside its profile rather than guessing.

    Source: §VI · p. 8

    Matrix insertion and assembly remain outside the verification claim until the CIVL model of PETSc stash and assembly behavior is validated.

    Source: §IV · p. 7

Abstract

from arXiv · show

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.

I. INTRODUCTION

PETSc is widely used in high-consequence scientific applications, yet extensive testing can miss subtle defects, and hand-written verification artifacts do not scale across its code base. The paper separates LLM contract generation from human certification and deterministic driver generation, building on CIVL and existing PETSc models.

I. INTRODUCTION

  • Extensive testing can miss subtle defects, while hand-written CIVL drivers, reference models, and supporting artifacts do not scale to PETSc’s code base.One-shot LLM driver generation is also risky because the generated harness is unverified and difficult to audit.Source: §I · p. 1
  • The pipeline limits LLM output to a short contract for human review, then deterministically generates a CIVL driver to check the implementation against the contract and, when available, a reference model.The three stages are LLM generation, human certification, and deterministic driver generation.Source: §I · pp. 1–2, Figure 1 · p. 2

A. Background on the CIVL model checker

  • CIVL explores symbolic inputs and compares an implementation with a trusted reference model when available, checking equivalence within specified bounds.Earlier CIVL verification of PETSc vector functions found two previously undiscovered bugs.Source: §I · p. 1, A. Background on the CIVL model checker · p. 2

B. PETSc

  • PETSc’s opaque handles, distributed storage, assembly state, and dynamic dispatch make drivers responsible for constructing legal symbolic objects and observing logical values.The pipeline retains the existing CIVL–PETSc object model and porting discipline while replacing hand-written drivers with contract-generated ones.Source: B. PETSc · p. 2

II. APPROACH

The approach separates language-and-modeling judgments from mechanical harness generation, with a human-certified contract as the boundary between them. A restricted PETSc-ACSL profile and dense logical object model give the deterministic compiler a defined translation target.

II. APPROACH

  • The design separates LLM-assisted behavior modeling from mechanical CIVL harness generation, using human inspection of a small contract as the boundary.The driver is difficult to audit when generated directly because it combines object construction, case splitting, frame checks, reference-model calls, and CIVL plumbing.Source: §II · pp. 2–3
  • Three stages turn documentation into verification: the LLM drafts a profile-bounded contract, an expert certifies it, and acsl2civl deterministically generates drivers or rejects unsupported constructs.CIVL checks each generated driver against the CIVL-compilable implementation port.Source: §II · p. 3

A. Symbolic representation: a PETSc contract language

  • The PETSc-ACSL profile uses a supported ACSL fragment with PETSc-specific predicates, translated by acsl2civl into CIVL-C driver code.The fragment supports clauses such as requires, assigns, and ensures.Source: A. Symbolic representation: a PETSc… · p. 3
  • Verification models each distributed matrix or vector as a dense row-major global image, abstracting away distributed storage and MPI communication.The profile supports scalar arithmetic, comparisons, conditionals, and object equality, but not reductions such as sums, norms, or dot products.Source: A. Symbolic representation: a PETSc… · p. 3

B. Stage 1: from documentation to a candidate contract

Stage 1 asks an LLM to draft a candidate contract from PETSc documentation using the current profile, while withholding the source repository. Stage 2 has a PETSc-aware expert certify the behavior and record justified decisions where documentation leaves gaps.

B. Stage 1: from documentation to a candidate contract

  • The LLM drafts a contract from the manual page, function prototype, and profile without repository access, to favor documentation-grounded specifications over implementation choices.The authors acknowledge that the model may nevertheless have prior knowledge of PETSc source code.Source: B. Stage 1: from documentation to a… · p. 3
  • When documentation leaves behavior unspecified, the candidate contract must make the gap and any resulting assumption explicit, and Stage 1 can be repeated after later-stage feedback.The Stage 1 prompt and resulting contract are archived; Stage 2 corrections are reflected in the certified contract.Source: B. Stage 1: from documentation to a… · pp. 3–4

C. Stage 2: human-certification

  • A PETSc-aware expert checks formulas against documentation and records justified decisions for ambiguities, such as allowing MatAXPY aliasing after reviewing related API behavior.Certification also records documented logical-collective obligations; rejected contracts are revised or regenerated, and acsl2civl performs mechanical profile checks before driver generation.Source: C. Stage 2: human-certification · p. 4

D. Stage 3: deterministic translation to a CIVL driver

acsl2civl deterministically translates supported contracts into CIVL drivers, with trust boundaries distinguishing certified contracts from checked artifacts. In the small experiments, aliased MatAYPX drivers expose a provable contract violation.

D. Stage 3: deterministic translation to a CIVL driver

  • acsl2civl parses contracts into a specification IR, derives admissible cases, and emits one CIVL driver per case.Drivers run CIVL-compatible ports that preserve verified implementation paths while removing unsupported features; only MatAXPY has a reference model.Source: D. Stage 3: deterministic translation… · p. 4

E. Trust boundaries

  • CIVL and the ports, PETSc module, and compiler are trusted; the LLM is not, and the human-certified contract states intended behavior.For MatAYPX, contract postconditions and frame conditions are the only correctness checks.Source: E. Trust boundaries · p. 4

III. EVALUATION

  • The small experiments exhaustively explore executions and symbolic inputs for 1–2 MPI processes and matrix dimensions M, N from 1 to 3.The explored modes are limited to those admitted by each certified contract.Source: §III · p. 4
  • Aliased MatAYPX drivers terminate at a provable contract violation, while distinct drivers pass in contract-only mode.Source: §III · p. 4
  • Certified contracts require 8–14 lines versus 38–176 generated-driver lines per function, exposing review surface but not review time.Source: §III · p. 5, Table IV · p. 5

A. Worked example: MatAXPY

The MatAXPY example shows how a certified contract is translated into drivers that exercise both aliasing cases and admitted nonzero-pattern hints. The dense model checks matrix values, while the drivers also check contract assertions and, where available, a reference model.

A. Worked example: MatAXPY

  • Because the documentation is silent on aliasing, review removes the generated separation requirement and retains the implementation’s distinct pointer-equality branch for same-handle inputs.The value formula remains coherent under aliasing, but the implementation takes a separate path when X and Y are the same handle.Source: A. Worked example: MatAXPY · p. 5
  • The contract admits DIFFERENT_NONZERO_PATTERN and UNKNOWN_NONZERO_PATTERN, while the dense model cannot represent or check the structural preconditions for SAME_NONZERO_PATTERN or SUBSET_NONZERO_PATTERN.The str argument is a nonzero-pattern hint used for internal optimization.Source: A. Worked example: MatAXPY · p. 5
  • Stage 3 generates four drivers spanning distinct or aliased handles and DIFFERENT_NONZERO_PATTERN or UNKNOWN_NONZERO_PATTERN; the distinct driver checks the reference result, frame, and contract assertions.The dense model checks numerical matrix values, not sparse-pattern claims.Source: A. Worked example: MatAXPY · pp. 5–6

B. Evolving the profile

The MatAXPY aliasing case illustrates how human review can refine the ACSL profile and deterministic compiler when documentation leaves behavior unresolved. Repeated contract patterns can then be encoded as mechanical Stage 3 rules.

B. Evolving the profile

  • The profile is extended when the same contract structure recurs, allowing Stage 3 to generate that structure mechanically.The MatAXPY aliasing split illustrates this human-in-the-loop refinement process.Source: B. Evolving the profile · p. 6
  • The refinement loop inspects the generated contract, identifies the unverified alias branch, resolves the documentation gap through human judgment, and mechanizes the alias split in acsl2civl.The reviewer removes the generated separated_mat clause, and Stage 3 then derives distinct and aliased drivers.Source: B. Evolving the profile · p. 6
  • Further applications may reveal recurring patterns that warrant explicit Stage 3 rules, increasing acsl2civl’s capabilities and reusability.Source: B. Evolving the profile · p. 6

C. Contract-only verification: MatAYPX and an aliasing bug

MatAYPX has no reference model, so its certified contract is the oracle for checking the implementation. The aliased drivers expose a provable violation: the implementation produces a different result from the documented behavior when X and Y are the same matrix.

C. Contract-only verification: MatAYPX and an aliasing bug

  • Because MatAYPX has no reference model, its certified contract is the sole oracle; review corrected the missing pre-state value and tested both admitted pattern hints.The dense model checks numerical results, not sparse-pattern claims, and Stage 3 derives distinct and aliased drivers.Source: C. Contract-only verification: MatAYPX… · p. 6
  • Aliased MatAYPX drivers produce a provable contract assertion violation, while distinct drivers pass in contract-only mode.With X = Y, scaling Y before adding X yields 2aY_old instead of the documented (1 + a)Y_old.Source: C. Contract-only verification: MatAYPX… · pp. 6–7
  • The documented behavior applies without an aliasing restriction, so the inconsistent aliased result is a bug rather than grounds to weaken the contract.MatAXPY, in contrast, explicitly handles aliased inputs and satisfies its documented equation.Source: C. Contract-only verification: MatAYPX… · p. 7

D. A conditional operation: MatFilter

The MatFilter example verifies its dense, non-compressing mode with a conditional, elementwise contract. Supporting that behavior required extending the ACSL profile and acsl2civl.

D. A conditional operation: MatFilter

  • In non-compressing mode, MatFilter zeroes entries whose magnitude is at most tol and preserves all other entries.The example sets both compress and keep to false; those modes are not yet supported.Source: D. A conditional operation: MatFilter · p. 7
  • The generated driver treats tol as a symbolic input, and support for symbolic PetscReal parameters and conditional expressions was added for this behavior.Relational comparisons and \abs were also added to the profile and translation tool.Source: D. A conditional operation: MatFilter · p. 7
  • The contract expresses the elementwise condition using a pre-state value, absolute value, comparison, and conditional expression, then lowers it to a CIVL-C assertion.Source: D. A conditional operation: MatFilter · p. 7

IV. SCOPE AND LIMITATIONS

The verification scope depends on modeling PETSc assembly state faithfully. Scalar vector stash support exists, but matrix stash support remains ongoing, leaving matrix insertion and assembly outside the verification claim.

IV. SCOPE AND LIMITATIONS

  • Elementwise algebraic routines such as MatAXPY admit direct pre- and post-state relations, but assembled state depends on AssemblyBegin/AssemblyEnd combining pending updates.Locally owned updates may apply immediately, while off-process updates remain in stash objects until assembly completes.Source: §IV · p. 7
  • CIVL models the scalar VecStash path, while extending stash support to matrices is ongoing.Sparse matrix stash modeling must account for rowwise storage, preallocation, duplicate entries, and insertion-mode rules.Source: §IV · p. 7
  • Matrix insertion and assembly remain outside the verification claim until the CIVL model can faithfully represent PETSc’s stash and assembly machinery.Reimplementing that machinery duplicates complex state and communication logic, which requires focused drivers and cross-checks of its own.Source: §IV · p. 7

V. RELATED WORK

The paper positions its approach among LLM-assisted specification and verification work, while emphasizing a restricted ACSL profile and human certification. Its evaluation finds a long-standing MatAYPX bug, and the conclusion outlines extensions to the toolchain.

V. RELATED WORK

  • Related LLM-verification work includes generated postconditions, natural-language translation tasks, and verifier-feedback or test-supported synthesis,,, [14].This work instead targets existing PETSc implementations and has an expert certify a compact documentation-derived contract before driver generation.Source: §V · p. 7
  • The approach supports only the ACSL fragment with explicit acsl2civl lowering rules, not general contract inference or full ACSL verification.Unsupported constructs are rejected rather than approximated.Source: §V · p. 7
  • A Frama-C plug-in could check syntax, typing, binding, and profile membership before export, but would not eliminate human review of documentation or policy decisions.A well-formed contract does not establish that it faithfully captures incomplete documentation.Source: §V · pp. 7–8

VI. CONCLUSIONS

  • The pipeline has the LLM propose a compact contract from PETSc documentation, a domain expert certify it, and a deterministic compiler generate CIVL drivers.The tool refuses contracts outside its restricted profile rather than guessing.Source: §VI · p. 8
  • A derived aliased case exposed a MatAYPX bug present since 1997: identical operand handles produce 2aY rather than (1 + a)Y.The evaluation also covered MatAXPY and non-compressing MatFilter, with conditional postconditions over real parameters added for MatFilter.Source: §VI · p. 8
  • Future work includes matrix assembly support, broader Mat and Vec operation coverage, lowering supported requires clauses into driver assumptions, and a Frama-C profile-checking plug-in.Source: §VI · p. 8

APPENDIX A ARTIFACT AND REPRODUCIBILITY

The appendix describes the artifact’s prompts, reviewed contracts, compiler, and CIVL–PETSc module, and notes that the artifact is supplementary material.

APPENDIX A ARTIFACT AND REPRODUCIBILITY

  • The artifact includes three versioned Stage 1 prompts, contracts corrected and certified during Stage 2 review, and the Stage-3 compiler and CIVL–PETSc module.The contracts were authored with Claude; their headers record review stamps.Source: Appendix A · p. 8

APPENDIX B ARTIFACT AVAILABILITY

  • The artifact is submitted as supplementary material, with a public archival URL to be added to the camera-ready version.Source: Appendix B · p. 8
Loading 2609.31687v1…