ProofWright: Towards Agentic Formal Verification of CUDA

TL;DR

ProofWright addresses the reliability gap in AI-assisted CUDA kernel generation by combining automated formal verification with LLM-based code generation. It introduces a VerCors Agent to establish memory safety and data-race freedom, and a Semantic Equivalence Framework backed by Rocq to prove that CUDA implementations semantically match PyTorch specifications. On KernelBench L1, ProofWright verified memory and thread safety for 74% of kernels and established semantic equivalence for 14% of kernels, with modest per-kernel overhead dominated by verification time. Together, these results demonstrate that scalable, automated formal verification of GPU code produced by LLMs is feasible, enabling trustworthy high-performance code without sacrificing developer productivity.

Abstract

Large Language Models (LLMs) are increasingly used to automatically generate optimized CUDA kernels, substantially improving developer productivity. However, despite rapid generation, these kernels often contain subtle correctness bugs and lack formal safety guarantees. Runtime testing is inherently unreliable - limited input coverage and reward hacking can mask incorrect behavior - while manual formal verification is reliable but cannot scale to match LLM output rates, creating a critical validation bottleneck. We present ProofWright, an agentic verification framework that bridges this gap by integrating automated formal verification with LLM-based code generation. ProofWright provides end-to-end guarantees of memory safety, thread safety, and semantic correctness for LLM-generated CUDA kernels. On KernelBench L1, ProofWright verifies safety properties for 74% of generated kernels, uncovers subtle correctness errors missed by conventional testing, and establishes semantic equivalence for a class of element-wise kernels. With a modest overhead of 3 minutes per kernel, ProofWright demonstrates that scalable, automated formal verification of LLM-generated GPU code is feasible - offering a path toward trustworthy high-performance code generation without sacrificing developer productivity.

Figures (11)

• Figure 1: VerCors Agent for establishing memory and thread safety for CUDA Programs. The LLM-generated CUDA kernels are first minimally preprocessed, and then the safety annotations are generated in a step-by-step fashion, according to the automatically crafted annotation guide. The annotated program is then verified by calling the VerCors tool.
• Figure 2: Semantic Equivalence Framework. The front-end captures the original specification in a graph-based IR form, and is translated to Rocq theorems. The agentic back-end explores alternative mathematical representations of the original specification specification, and leverages them to generate low-level VerCors annotations.
• Figure 3: Operations Graph IR generated by Pytorch Static Analyzer for RMS. The input tensor $x \in \mathbb{R}^{16 \times 64 \times 256 \times 256}$ is squared, reduced across the channel dimension, stabilized with an epsilon constant, square-rooted, and finally broadcast-divided with the original tensor to produce the normalized output.
• Figure 4:
• Figure 6: Where does the VerCors Agent spends its time? Average Agent time breakdown for the Claude-4-Sonnet baseline on KernelBench-L1. Most of the time was spent in verification (up to 194 s for convolution operations) and annotation generation ($\sim$90 s for reduction and normalization kernels), while preprocessing remained relatively lightweight across all categories.