ProofWright: Towards Agentic Formal Verification of CUDA

• Testing can miss data races, out-of-bounds accesses, and reward-hacked kernels despite compilation and functional-test success.Rare inputs and synchronization-sensitive behaviors can evade validation, while kernels may pass tests without implementing the intended specification.Source: §1 · p. 2
• Formal verification is needed because dynamic testing and symbolic execution lack completeness guarantees and do not scale easily to high-integrity GPU applications.Existing approaches may be expensive, fail to examine all paths or thread interleavings, or require substantial expert effort.Source: §1 · p. 2
• ProofWright combines an agentic safety-verification framework with an agentic semantic-equivalence framework for LLM-generated CUDA kernels.The safety framework uses VerCors to prove memory safety and data-race freedom, while the equivalence framework uses static analysis, tensor-operation abstractions, and Rocq.Source: §1 · p. 3
• The framework evaluates generated CUDA kernels against PyTorch specifications using automated formal reasoning rather than testing alone.Its evaluation uses KernelBench, a benchmark of PyTorch programs targeting equivalent and performant CUDA kernels.Source: §1 · pp. 1, 3

2.1 Agentic Systems for GPU Code Generation & Optimization

• Agentic GPU systems generate optimized kernels from high-level specifications and iteratively refine them using compiler, testing, analysis, profiling, or LLM feedback.PyTorch serves as a structured specification and reference implementation in KernelBench.Source: §2.1 · p. 3

2.2 Shortcomings of Current Testing Methodologies: False Negatives, Code Coverage, Compatibility Issues

• Input-based dynamic testing can miss concurrency bugs that occur only for particular input sizes or thread-block configurations.A vectorized sigmoid kernel passed compilation and multiple unit tests even though tail processing caused cross-block write races when the input length was not divisible by four.Source: §2.2 · p. 4
• Symbolic execution explores feasible paths with SMT constraints but supports only simple atomic operations and does not scale beyond smaller kernels.It therefore improves coverage relative to ordinary testing without providing a scalable solution for modern GPU kernels.Source: §2.2 · p. 4
• Existing testing techniques may also accept kernels that pass tests while failing to implement their intended specification.A generated vector-add kernel illustrated how semantic misbehavior and reward hacking can survive compilation and unit tests.Source: §2.2 · p. 4

2.3 VerCors Program Verifier

• VerCors is a deductive verifier that proves CUDA memory safety and data-race freedom using contracts and permission-based concurrent separation logic.Annotations describe permission splits across threads, while verification checks disjointness and bounds of accessed locations.Source: §2.3 · p. 5
• VerCors verification can require helper functions, frame statements, or other hints for complex indexing, and some correct programs may remain unverifiable.Disjointness and in-bounds reasoning for thread accesses is undecidable in general.Source: §2.3 · p. 5

2.4 Rocq Theorem Prover

• Rocq is an interactive theorem prover whose Gallina language supports mathematical specifications, dependently typed programs, and machine-checkable proofs.Its value here is providing a formal representation for reasoning about functional behavior.Source: §2.4 · p. 6, Figure 1 · p. 6

• ProofWright establishes memory safety, thread safety, and semantic equivalence for LLM-generated CUDA code within the agentic generation workflow.The framework is designed to provide formal guarantees after candidate kernels have been generated and refined.Source: §3 · p. 6

Agentic Formal Verification Framework (§4)

• The VerCors agent generates annotations and verifier hints using a knowledge base, an evolving annotation guide, and a database of known errors and fixes.These components support generalization across verification experiences without manual annotation intervention.Source: §3 · p. 6

Agentic Semantic Equivalence Framework (§5)

• The semantic-equivalence framework extracts computation graphs, maps operations to mathematical properties, and uses a Rocq agent to construct proofs against the user specification.Verified theorems are lowered into program annotations and validated by a formal verifier.Source: §3 · pp. 6–7

Deployment

• ProofWright is intended as a later-stage, high-guarantee filter after faster compilation and unit-test checks have narrowed the candidate set.This deployment pattern accommodates pipelines that explore many kernel variants per iteration.Source: §3 · p. 7

• Formal verification prevents incorrect annotations or proofs from producing a verified result because failed formal obligations simply fail verification.The stated reliability mechanism is rejection of unverifiable claims rather than acceptance based on agent output alone.Source: §3 · p. 7

4 Agentic Formal Verification Framework: Establishing Thread & Memory Safety Guarantees

• The VerCors Agent preprocesses LLM-generated CUDA, generates annotations step by step using an Annotation Guide, and invokes VerCors to verify the annotated kernel.The workflow is iterative and feedback-driven.Source: §4 · p. 7, Figure 2 · p. 7

4.1 Verification Procedure

• The agent infers weakest satisfiable preconditions for safe invocation, while VerCors checks safety throughout execution without requiring meaningful postconditions.Accepted contracts imply that invocations satisfying the preconditions are safe; rejected kernels are conservatively treated as unsafe.Source: §4.1 · p. 8
• The agent identifies memory reads and writes, expresses thread-dependent locations and conditions, and uses helper functions and permission annotations to guide bounds and solver reasoning.It also infers array sizes, block and grid constraints, parameter bounds, and permission changes across barriers.Source: §4.1 · pp. 8–9

4.2 Tackling Low-Resource VerCors Syntax

• The VerCors knowledge base combines documentation, verified CUDA examples, and error-fix pairs so the agent can generate low-resource syntax and iteratively repair failed annotations.Repair entries pair original code, verifier errors, human explanations, and corrected code.Source: §4.2 · p. 9, §4.2.1 · p. 9

4.2.1 VerCors Knowledge Base: In-Context Learning.

• The static knowledge base does not generalize reliably to new control-flow, data-mapping, or synchronization patterns and may repeat prior errors without learning from experience.These limitations motivate a dynamic Annotation Guide.Source: §4.2.2 · p. 10

4.2.2 VerCors Annotation Guide: Learning from Experience.

• The dynamic Annotation Guide distills few-shot examples and past verification experience into an updateable recipe for generating VerCors-compatible specifications across CUDA kernel structures.The guide is approximately ∼9.5K tokens and can incorporate newly discovered verification patterns.Source: §4.2.2 · pp. 10–11
• The learned guide specializes verification by kernel family and thread-to-data mapping, generating helper functions and distinct permission, indexing, synchronization, and bounds strategies.It also balances fixed and parameterized block and grid dimensions while enforcing pointer, dimension, and allocation constraints.Source: §4.2.2 · pp. 10–11

5 Agentic Semantic Equivalence Framework: Proving Functional Correctness

• ProofWright extracts a PyTorch computation graph, translates it into Rocq, synthesizes a Rocq specification for CUDA, proves equivalence, and generates VerCors functional annotations.The final VerCors check tests whether the CUDA kernel satisfies the functional specification.Source: §5 · p. 11

5.1 Front-End: Translating Pytorch Specification to Rocq

• The semantic-equivalence front end contains the static analyzer, MLRocq, and a PyTorch-to-Rocq translator, and it excludes LLMs from formal specification construction.This design keeps the specification-generation stage independent of LLM components.Source: §5.1 · p. 12
• The PyTorch Static Analyzer represents operations as graph nodes with data-dependency edges and tensor metadata, producing an intermediate representation for formal translation.It uses torch.fx to symbolically trace and refine the graph with shapes and auxiliary parameters.Source: §5.1.1 · p. 12

5.1.2 MLRocq Library.

• MLRocq provides formal definitions and proofs for nearly one hundred PyTorch operations, using scalar definitions recursively across tensors and including over 200 validation tests.Current definitions are mostly restricted to integer and real data types to simplify proof construction.Source: §5.1.2 · pp. 12–13

5.1.3 Pytorch-to-Roq Translator.

• The translator maps each graph node to a typed Rocq definition using tensor metadata, preserves computational semantics, and stores completed proofs in MLRocq to avoid recomputation.The resulting specification supports downstream theorem generation and equivalence proofs.Source: §5.1.3 · p. 13

5.2 Backend: Proving Semantic Equivalence

• The Semantic Equivalence Agent constructs Rocq theorems and proofs for CUDA representations, then lowers the verified specification into VerCors annotations embedded in the generated kernel.A successful VerCors verification indicates intended output behavior relative to the original PyTorch specification; failure identifies deviations for analysis.Source: §5.2 · pp. 14–15
• The Rocq Agent proves equivalence between two ReLU implementations by case analysis on scalar inputs and induction over tensor dimensions.The result extends scalar equivalence to n-dimensional tensors.Source: §5.2 · pp. 14–15
• The current lowering from Rocq definitions to VerCors annotations is not guaranteed correct for all GPU-kernel types because an LLM performs that step.The authors manually verified the lowered annotations in evaluation and identify a procedural compiler as future work.Source: §5.2 · p. 15

6 Evaluation

• The evaluation tested ProofWright on KernelBench L1 kernels generated by Claude-4-Sonnet and GPT-5-Codex across five research questions covering safety, overhead, ablations, specification capture, and trusted semantic-equivalence coverage.Experiments used a MacBook Pro with a 14-core Apple M4 Pro processor and minimally extended VerCors for required CUDA constructs.Source: §6 · pp. 15–16

6.1 Memory & Thread Safety: Extent of Coverage (RQ1)

• 74% of 100 KernelBench L1 kernels received automatically established memory and thread-safety guarantees, with failures mainly involving unsupported patterns or solver instability.The agent generalized permission patterns to unseen kernels, while non-affine indexing and SMT instability remained important failure sources.Source: §6.1 · pp. 16–17

6.2 Memory & Thread Safety: Agentic Overheads (RQ2)

• Annotation generation took approximately 90 s with minimal preprocessing, while verification dominated runtime at up to 194 s for complex kernels.Verification dominated matrix multiplication, convolution, and cumulative operations; annotation was comparatively costly for pooling, reduction, loss, and normalization.Source: §6.2 · pp. 18–19, Figure 8 · p. 18

6.3 Memory & Thread Safety: Ablation Study (RQ3)

• The agent verified no kernels without the knowledge base or annotation guide, and only 13 kernels with the knowledge base plus few-shot examples.The ablation indicates that reusable verification knowledge and persistent annotation guidance are necessary for effective verification rather than prompt engineering alone.Source: §6.3 · pp. 19–20, Figure 9 · p. 19

6.4 Semantic Equivalence: Capturing Functional Specification (RQ4)

• The semantic-equivalence front end extracted operation-level computation graphs from 200 PyTorch programs and mapped approximately 92% of KernelBench L1 operations through 99 MLRocq implementations.The static analyzer represented high-level functional specifications as computation graphs for subsequent formal reasoning.Source: §6.4 · pp. 20–21, Figure 10 · p. 20, Figure 11 · p. 20

6.5 Semantic Equivalence: Extent of “Trusted" Coverage (RQ5)

• Full semantic equivalence was established for 14% of KernelBench L1 kernels, with partial equivalence for an additional 3%.The fully verified cases were primarily element-wise kernels with one-to-one thread-to-output mappings, while reductions and cross-thread dependencies remained challenging.Source: §6.5 · pp. 21–22, Figure 12 · p. 21

• VerCors currently supports shared-memory accesses and synchronization primitives such as _syncthreads, but not tensor-core instructions including mma and wgmma.This limits verification of modern high-performance CUDA kernels using unsupported features.Source: §7 · p. 22

• Dynamic instrumentation and symbolic execution can detect unsafe behavior, but they remain unsound because they do not consider all possible executions.Compute Sanitizer and GKLEE illustrate lower-overhead approaches that strengthen testing without providing complete guarantees.Source: §8 · pp. 22–23
• ProofWright focuses on sound verifiers such as GPUVerify and VerCors, whose user annotations provide an interface for LLM-guided verification.The related-work discussion identifies integration with tools lacking simple text interfaces as an open question.Source: §8 · p. 23
• LLM-based verification systems such as Laurel and AutoVerus generate or repair proofs, while ProofWright targets CUDA and additionally addresses memory safety, data-race freedom, and functional specifications extracted from high-level implementations.AutoVerus assumes existing Verus specifications and benefits from Rust’s type-system guarantees, whereas ProofWright reasons about CUDA-specific safety properties.Source: §8 · p. 23
• Other verifiable-code-generation methods increase confidence but still require a human or another entity to check whether generated specifications match the original intent.ProofWright separates code generation from verification, while its outputs could provide feedback to generation systems.Source: §8 · p. 23
• ProofWright uses LLMs to guide automated program verifiers without encoding target-program semantics directly in the theorem prover’s language.This relates to prior work showing that proof abstraction and reuse can improve LLM proof generation over time.Source: §8 · p. 23

• ProofWright’s methodology relies on a knowledge base, annotation guide, and verifier feedback to enable automated verification of GPU kernels.The conclusion presents these components as the framework’s conceptual basis.Source: §9 · p. 23
• 74% of KernelBench L1 kernels had verified thread and memory safety, while 14% had established semantic equivalence with relatively low overhead and no model training.These results support the framework’s effectiveness across safety and semantic-correctness goals.Source: §9 · p. 24
• Naive prompting and limited few-shot examples often produce pattern matching rather than correct reasoning, whereas knowledge bases and annotation guides are essential for generalization.This conclusion is drawn from the framework’s verification-agent experiments.Source: §9 · p. 24
• Future work will extend VerCors support for more CUDA features and develop analytical Rocq-to-VerCors annotation translation to improve semantic-equivalence reliability.These directions target broader kernel coverage and more reliable specification lowering.Source: §9 · p. 24