ProofWright: Towards Agentic Formal Verification of CUDA
This addresses a critical validation bottleneck for developers using LLMs to generate optimized CUDA kernels, offering scalable formal verification to ensure trustworthy high-performance code generation.
The paper tackles the problem of verifying correctness in LLM-generated CUDA kernels, which often contain subtle bugs, by introducing ProofWright, an agentic verification framework that integrates automated formal verification with LLM-based code generation. The result shows that ProofWright verifies safety properties for 74% of generated kernels with a modest overhead of 3 minutes per kernel, uncovering errors missed by conventional testing.
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.