# ProofWright: Towards Agentic Formal Verification of CUDA

arXiv: https://arxiv.org/abs/2511.12294 · HTML: https://mlsanity.com/paper/2511.12294/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 13 of its 43 references that are in the map.
- First posted on arXiv 15 Nov 2025.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

## Builds on (most cited first, 13 of 13)

- [KernelBench: Can LLMs Write Efficient GPU Kernels?](https://mlsanity.com/paper/2502.10517/) (2025)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [EffiLearner: Enhancing Efficiency of Generated Code via Self-Optimization](https://mlsanity.com/paper/2405.15189/) (2024)
- [LLM-Vectorizer: LLM-based Verified Loop Vectorizer](https://mlsanity.com/paper/2406.04693/) (2024)
- [PerfCodeGen: Improving Performance of LLM Generated Code with Execution Feedback](https://mlsanity.com/paper/2412.03578/) (2024)
- [Saarthi: The First AI Formal Verification Engineer](https://mlsanity.com/paper/2502.16662/) (2025)
- [Dafny as Verification-Aware Intermediate Language for Code Generation](https://mlsanity.com/paper/2501.06283/) (2025)
- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)
- [Permission-Based Separation Logic for Multithreaded Java Programs](https://mlsanity.com/paper/1411.0851/) (2014)
- [HiRace: Accurate and Fast Source-Level Race Checking of GPU Programs](https://mlsanity.com/paper/2401.04701/) (2024)

## Built on by (most cited first, 9 of 9)

- [Reward Hacking in the Era of Large Models: Mechanisms, Emergent Misalignment, Challenges](https://mlsanity.com/paper/2604.13602/) (2026)
- [Security in the Age of AI Teammates: An Empirical Study of Agentic Pull Requests on GitHub](https://mlsanity.com/paper/2601.00477/) (2026)
- [M2K: Making the Model-Kernel Interface Explicit for Reliable CUDA Kernel Verification](https://mlsanity.com/paper/2603.24595/) (2026)
- [Ave: Guiding Agentic GPU Optimization Using Data-Flow Invariants](https://mlsanity.com/paper/2604.18616/) (2026)
- [Don't Regenerate, Debug: A Domain-Specific Agent for Repairing Near-Miss Hardware Operators](https://mlsanity.com/paper/2608.02712/) (2026)
- [PTXBench: Benchmarking and Adapting LLMs for GPU Kernel Optimization with Architecture-specific PTX](https://mlsanity.com/paper/2608.17379/) (2026)
- [MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs](https://mlsanity.com/paper/2609.19391/) (2026)
- [The Output-Space Hypothesis: Enumerative Equivalence Checking for Tensor Programs](https://mlsanity.com/paper/2609.19611/) (2026)
- [RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof](https://mlsanity.com/paper/2610.05683/) (2026)

## Abstract (arXiv)

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.