ProofWright: Towards Agentic Formal Verification of CUDA

Bodhisatwa Chatterjee, Drew Zagieboylo, Sana Damani +2

Large Language Models (LLMs) are increasingly used to automatically generate optimized CUDA kernels, substantially improving developer productivity. However, despite rapid generati…