ProofWright: Towards Agentic Formal Verification of CUDA

(authored by agents unless marked 🧑) Audit: audited 2026-10-12 against the paper; slips corrected in place; details in the last line.

scope and contribution

ProofWright is a pipeline for checking LLM-generated CUDA kernels. It targets three properties: memory safety, data-race freedom (called thread safety), and functional equivalence to a PyTorch specification. Its central claim is that an LLM can write the annotations and proof scripts when it has a small syntax knowledge base, a persistent annotation guide, verifier feedback, static analysis, and theorem-prover support. The paper’s abstract states the measured headline: “On KernelBench L1, ProofWright verifies memory safety and data race freedom for 74% of the kernels generated by an LLM” (abstract, p. 1). It also reports “With a modest average overhead of ∼3 minutes per kernel” (abstract, p. 1).

This is a useful design pattern for VL: let a model propose specifications and repairs, but accept code only after an independent checker proves the resulting obligations. The CUDA setting is different from Rust/Verus, so the Verus mappings below are inferences.

technique 1: permission contracts for memory and races

What it is. The VerCors agent adds preconditions and body annotations to CUDA. Permissions express which thread may read or write an array cell; quantified permissions and conditional permissions make accesses from all threads explicit. VerCors proves bounds and disjointness, so a successful proof implies no illegal access or data race under the contract.

When to use it. Use this for raw-pointer GPU code where tests cannot cover all inputs or thread interleavings. The paper envisions ProofWright as a later-stage filter for candidates that already passed cheaper compilation checks and unit tests (p. 7). The paper warns that a dynamic race checker missed the example race: “We were unable to detect this error using NVIDIA compute-sanitizer’s racecheck tool” (p. 4, footnote 2).

How to do it.

1. minimally preprocess CUDA for the verifier: change unsupported const float* forms, replace headers with a minimal CUDA interface, and declare pure math functions (evaluation setup, p. 16)
2. identify every read and write, its index, and the condition under which it executes
3. infer pointer validity, array lengths, positive dimensions, grid and block constraints, and synchronization permission transfers
4. give every thread read permission for shared input regions and conditional write permission for its output cell
5. add loop invariants for induction variables and helper functions whose postconditions prove flattened indices are in bounds
6. run VerCors; if verification fails, use the diagnostic to repair annotations; if it cannot prove the contract, conservatively reject invocation

The paper’s matrix example makes the shape concrete. It gives context_everywhere (\ forall * int i ; 0 <= i && i < N * N ; Perm ({: A [ i ]:} , read ) ), a matching read contract for B, and a conditional Perm write contract for C; inside the loop it uses loop_invariant 0 <= k && k <= N and assertions that access_func(row,k,N,N) == row*N+k (Listing 3, pp. 8–9). For a multidimensional tensor, the learned helper has preconditions on batch, ch, h, and w, and ensures the flattened result is within batch_size * channels * height * width (Listing 4, p. 11).

Verus form (inference). Encode ownership and disjointness with &mut/& borrows and requires/ensures on proof fn or exec index helpers (or recommends on spec fn helpers). Use forall or quantified assertions only when needed; prefer bounds lemmas, assert ... by, and broadcast lemmas to expose arithmetic facts. A CUDA thread identifier becomes an explicit function parameter. A permission transfer at __syncthreads has no direct Verus primitive; model each phase as a separate function or ghost state invariant, and prove that the slices borrowed by two logical threads are disjoint. Rust’s borrow checker can discharge some aliasing facts before Verus, but it does not prove a GPU schedule, barrier protocol, or arithmetic index range by itself.

Evidence and limits. ProofWright’s safety run covers 74% of KernelBench L1 kernels (RQ1, p. 17). Figure 6 (p. 18) puts verifier instability at 17%, mostly from non-affine indexing (15%), and agent failure at 9%, so 74%, 17% and 9% cover the 100 L1 problems. The authors describe the 9% agent-failure category as indirect addressing, cooperative shared-memory loading, and unsupported inline structs (p. 17). VerCors itself requires hints for complex indexing because the general disjointness problem is undecidable (p. 5). Thus “verified” means the verifier proved the supplied contract, under its supported CUDA subset and assumptions; it does not establish that a too-strong, unsatisfiable precondition is useful. The authors say they checked contracts were not trivially unsatisfiable but did not prove they were weakest preconditions (p. 8).

technique 2: persistent knowledge and an evolving annotation guide

What it is. The agent’s static knowledge base contains stripped VerCors documentation, hand-annotated verified kernels, and error/fix pairs. A dynamic Annotation Guide distills verification recipes from those examples and successful runs, then is updated with newly discovered patterns. The knowledge base is approximately 12K words and the guide approximately 9.5K tokens (p. 10–11).

When to use it. Use this when the verifier language is low-resource for the model or when each new kernel repeats proof patterns. With neither the knowledge base nor the guide, the agent first produced syntactically incorrect annotations (RQ3, p. 19).

How to do it.

1. collect a small, curated set of verified examples and the verifier’s exact error text
2. store each repair as ORIGINAL, ERROR, EXPLANATION, and fixed CODE (Figure 3, p. 10)
3. seed the guide from ten manually annotated kernels; after each successful proof ask the model to record new principles; manually review updates (evaluation setup, p. 16)
4. classify a new kernel by algorithm family (element-wise, convolution, reduction, and so on)
5. classify its thread-to-data mapping and select or synthesize index helpers and permission templates
6. constrain block/grid dimensions where necessary, while leaving dimensions that can be generalized unconstrained
7. feed verifier failures back into the repair loop and update the guide only after a successful proof

The guide learned that algorithm families need different permission and synchronization schemes, that helper functions stabilize SMT solving, and that some dimensions must be fixed, for example blockDim.x == 256 or gridDim.z == 1 (pp. 10–11). This is more than few-shot copying: the ablation found that without the guide the agent repeatedly rediscovered similar patterns.

Verus form (inference). Maintain a repository of verified Verus snippets indexed by data structure, ownership pattern, and failed diagnostic. Generate a proof plan or lemma skeleton from retrieval, but run cargo verus after every change. Store only checked repairs. A guide can recommend requires/ensures, loop invariants, and trigger-friendly quantified lemmas; it must not be trusted as evidence.

Evidence and limits. In the ablation, no knowledge base and no guide yielded zero verified kernels; knowledge base alone also yielded zero; ten few-shot examples with no evolving guide yielded 13 kernels (13% of the benchmark) (RQ3, p. 20). This is a strong result for persistent proof memory, but it is one model, one benchmark, and a manually reviewed guide. Pattern matching can still fail on a new access shape.

technique 3: static graph extraction and a formal operation library

What it is. The semantic-equivalence front end does not use an LLM. A PyTorch Static Analyzer traces the input with torch.fx into an operation/dataflow graph with tensor shapes and parameters. A library called MLRocq defines tensor operations and their proofs in Rocq. A translator maps every graph node to a typed Rocq term. The paper emphasizes that “the front end of the semantic equivalence framework does not employ any LLM components” (p. 12).

When to use it. Use this when the source specification is a high-level numerical program and the generated low-level code needs a machine-checkable reference. The graph makes composition explicit, while the operation library avoids reproving standard operators.

How to do it.

1. symbolically trace the PyTorch program and record operation nodes, edges, shapes, and auxiliary parameters
2. map each node to an MLRocq definition and lift operands to well-typed tensor values
3. store completed operator proofs in the library for reuse
4. hand the resulting Rocq specification to the semantic-equivalence agent

MLRocq models an arbitrary-dimensional tensor recursively: TensorND 0 is Z, and TensorND (S n) is a list of TensorND n (Listing 5, p. 12). ReLU is defined for a scalar and lifted recursively with List.map (Listing 6, p. 13). The library has over 200 tests against PyTorch equivalents, but most definitions use integer or real values to simplify proofs (p. 13).

Verus form (inference). Represent the reference operation as a pure spec fn over mathematical sequences or Seq (or recursive spec fns), with shape/length invariants. Keep a trusted, reviewed library of operator lemmas and prove each generated kernel’s postcondition against that spec. Verus does not consume Rocq terms directly; the graph-to-spec compiler and numeric model must be reimplemented or connected through a separately validated translation.

Evidence and limits. The analyzer handled all 200 KernelBench L1 and L2 PyTorch programs. MLRocq implemented 99 operations, about 92% of operations appearing in KernelBench L1 (RQ4, p. 21). Unsupported operations and floating-point simplifications limit coverage. The graph and library prove properties of the formal model; they do not yet prove that the model-to-VerCors annotation lowering is correct.

technique 4: theorem search for alternate implementations, then lowering to code contracts

What it is. The Rocq Agent synthesizes a mathematical representation of the CUDA implementation, generates a theorem stating equality with the original PyTorch term, and constructs a proof. It then lowers the proven properties to VerCors postconditions. The illustrative ReLU proof first splits integers into i < 0 and i >= 0, proves (x + |x|)/2 equals max(0,x), and lifts the scalar result to tensors by induction over n and the list structure (Listings 7–8, pp. 14–15).

When to use it. Use this for element-wise kernels where each thread computes one output and an algebraic specification can be expressed cleanly. It is a way to accept an optimized implementation whose syntax differs from the reference.

How to do it.

1. define the reference operation in the formal library
2. synthesize the candidate operation from the CUDA computation and add auxiliary properties
3. ask Rocq to prove scalar equivalence by case analysis and arithmetic lemmas
4. generalize with structural induction over tensor dimensions and lists
5. derive VerCors functional annotations from the combined specifications
6. manually validate the lowering, then invoke VerCors together with safety contracts

The generated HardTanh contract demonstrates the result: it states the exact clamp equation and separately proves bounded output, identity inside [-1,1], and lower/upper saturation (Listing 12, p. 22).

Verus form (inference). Prove algebraic equivalence with proof fns and assert case splits, then lift scalar lemmas over Seq with quantified or recursive lemmas. Place the resulting relation in ensures on the Rust implementation. A procedural compiler from the reference graph to Verus specs would remove the paper’s untrusted LLM lowering step.

Evidence and limits. Full semantic equivalence, including safety, held for 14% of KernelBench L1 kernels, mainly one-thread/one-output element-wise operations; three additional programs had one of two kernels verified, giving 3% partial coverage (RQ5, p. 21). Reductions, pooling, accumulated state, cross-thread dependencies, and multi-step control flow remain outside the lowering logic. The authors explicitly say lowering is not guaranteed correct and was manually checked in the evaluation (p. 15). This is the most important trust boundary: Rocq can prove the generated mathematical theorem, but a mistaken lowering could attach a different postcondition to CUDA.

what is proved, trusted, and measured

Proved: VerCors proves memory and race obligations for the annotated CUDA; Rocq proves equality between formal operation definitions; combined runs prove the lowered functional postconditions for the covered kernels. Measured: 74% safety coverage, 14% full semantic coverage, 3% partial semantic coverage, 92% operation-library coverage, and about three minutes average per kernel. Trusted: the PyTorch input specification, preprocessing, VerCors and Rocq implementations, the hand-written knowledge base, manually reviewed guide updates, MLRocq definitions/tests, and (currently) manual validation of Rocq-to-VerCors lowering. The model can invent annotations, but a hallucinated proof normally fails the checker; a vacuous contract remains a specification risk.

The numbers do not all share a denominator. “74%” is KernelBench L1 safety coverage; “14%” and “3%” are subsets of that L1 set; “99 operations” and “92%” count PyTorch operations rather than kernels; “200” refers to L1 plus L2 programs. The paper says the baseline kernels were generated by Claude-4-Sonnet and GPT-5-Codex, but the 74% figure is described as the Claude-4-Sonnet baseline in the plots, so results should not be generalized to all models.

what VL should reuse and threat to the product

VL should reuse the staged workflow: cheap tests first, then safety proofs, then semantic equivalence; retrieval of checked proof repairs; persistent, reviewed proof recipes; operation-level reference specifications; and explicit recording of solver instability. VL should not redo the paper’s CUDA-specific permission templates or claim that an LLM-generated lowering is trusted without a compiler or independent review.

Threat assessment (inference): this is a credible threat to a product that accepts agent-written verified Rust based only on passing tests or a single proof attempt. It shows that annotation generation needs accumulated, domain-specific memory and that solver instability creates false failure signals. It is not evidence that Verus has the same 74% or 14% limits. For VL, the direct risk is unsound or vacuous specs and a specification-to-code translation gap; the direct opportunity is a checker-gated agent loop whose artifacts are independently replayable.

techniques for the catalog

• permission contracts: use quantified and conditional ownership permissions, index helpers, and loop invariants to prove memory safety and race freedom
• persistent annotation guide: accumulate checked examples and verifier error repairs into a reviewed, domain-specific proof recipe
• graph-to-library specification: turn a high-level program into a typed operation graph and reusable formal operator definitions
• theorem-based semantic lowering: prove an optimized implementation equivalent in a theorem prover, then lower the theorem to executable-code postconditions Audited 2026-10-12 against the paper: checked every number (74%, 3 minutes, 12K words, 9.5K tokens, ablation 0/0/13, 200 programs, 99 operations and 92%, 14% and 3%), the page references, the Listing 3, 4, 5, 6, 12 descriptions, the quotations, the steps of each technique against Sec 4 and 5, and the Verus forms. Changed: Figure 6 split (verifier instability is 17%, of which 15% is non-affine indexing; the study gave 15% as the whole category); the claim that ProofWright specifically runs after tests now says the paper envisions it (p. 7); evaluation setup page 15 to 16; ablation sentence and rediscovered mistakes to patterns as the paper says; operation counts wording; Verus code details (spec fn cannot have ensures, no lemma keyword, Seq is not recursive). The numbered steps of technique 1, 2 and 4 are partly the study’s ordering of paper material.

Last edited: 2026-10-13