ProofWright: Towards Agentic Formal Verification of CUDA

• URL: http://arxiv.org/abs/2511.12294v1
• Date: Sat, 15 Nov 2025 17:06:50 GMT
• Title: ProofWright: Towards Agentic Formal Verification of CUDA
• Abstract summary: Large Language Models (LLMs) are increasingly used to automatically generate optimized kernels.<n>Despite rapid generation, these kernels often contain subtle correctness bugs and lack formal safety guarantees.<n>We present ProofWright, an agentic verification framework that bridges this gap by integrating automated formal verification with LLM-based code generation.
• Score: 1.8946520856889382
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis [14.825615940318038]
  ZkEVMs generate zero-knowledge that guarantee off-chain execution correctness.<n> subtle implementation bugs can lead to valid proofs certifying semantically faulty states.<n>Formal verification via SMT solvers can prevent this, but is bottlenecked by specification.<n>We propose Veri Synth, a framework that synthesizes executable Python/Z3 verification models from Rust.
  arXiv  Detail & Related papers  (2026-07-22T06:20:36Z)
• Harness Engineering for LLM-Driven GPU Kernel Generation [1.375573703671189]
  Large language models (LLMs) can assist GPU kernel generation, but their practical effectiveness depends on whether generated code can be reliably constrained, validated, profiled, and selected.<n>This paper presents a harness-centered system for LLM-driven GPU kernel optimization in the MLSys 2026 FlashInfer AI Kernel Generation Contest.
  arXiv  Detail & Related papers  (2026-07-20T14:14:14Z)
• Copper: Unifying Correctness and Performance Specification in Code Generation [1.799370552205315]
  We present Copper, a framework that combines formal verification with performance-aware specification.<n>Our approach integrates AI-driven code synthesis with formal verification tools, and automated performance profiling loops.
  arXiv  Detail & Related papers  (2026-07-03T09:19:34Z)
• Fast-dLLM++: Fréchet Profile Decoding for Faster Diffusion LLM Inference [45.385819280687514]
  We propose textbfFast-dLLM++, a training-free extension that introduces emphFréchet profile decoding.<n>Fast-dLLM++ leaves the model, diffusion process, and cache implementation entirely unchanged.<n>Experiments on GSM8K, MATH, HumanEval, and MBPP with the LLaDA-8B model show that the theoretical improvement translates directly into empirical gains.
  arXiv  Detail & Related papers  (2026-06-01T23:18:59Z)
• SecureForge: Finding and Preventing Vulnerabilities in LLM-Generated Code via Prompt Optimization [61.91729298584227]
  We introduce SecureForge, an automated pipeline that audits security risks of frontier models and produces auditing-informed secure system prompts.<n>SecureForge first identifies benign prompts that produce statically detectable vulnerabilities, and then amplifies them into a large synthetic prompt corpus of diverse scenarios.<n>On frontier models, SecureForge yields a statistically significant improvement in both unit test success and output security, with output vulnerabilities reduced by up to 48%.
  arXiv  Detail & Related papers  (2026-05-08T18:40:47Z)
• SecPI: Secure Code Generation with Reasoning Models via Security Reasoning Internalization [50.71047638695205]
  Reasoning language models (RLMs) are increasingly used in programming.<n>Yet, even state-of-the-art RLMs frequently introduce critical security vulnerabilities in generated code.<n>We present SecPI, a fine-tuning pipeline that teaches RLMs to internalize structured security reasoning.
  arXiv  Detail & Related papers  (2026-04-04T04:29:11Z)
• Outrunning LLM Cutoffs: A Live Kernel Crash Resolution Benchmark for All [57.23434868678603]
  Live-kBench is an evaluation framework for self-evolving benchmarks that scrapes and evaluates agents on freshly discovered kernel bugs.<n> kEnv is an agent-agnostic crash-resolution environment for kernel compilation, execution, and feedback.<n>Using kEnv, we benchmark three state-of-the-art agents, showing that they resolve 74% of crashes on the first attempt.
  arXiv  Detail & Related papers  (2026-02-02T19:06:15Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  Inference-time compute has re-emerged as a practical way to improve LLM reasoning.<n>Most test-time scaling (TTS) algorithms rely on autoregressive decoding.<n>We propose Prism, an efficient TTS framework for dLLMs.
  arXiv  Detail & Related papers  (2026-02-02T09:14:51Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• Counting Without Running: Evaluating LLMs' Reasoning About Code Complexity [2.7389338551082605]
  We develop a benchmark to test Large Language Models (LLMs) for anticipating performance bottlenecks.<n>FLOPBench predicts single and double-precision FLOP counts for 577 kernels.<n>Our results positionFLOPBench as a focused testbed for developing LLM tooling.
  arXiv  Detail & Related papers  (2025-12-04T01:03:20Z)
• DUALGUAGE: Automated Joint Security-Functionality Benchmarking for Secure Code Generation [18.208257676875586]
  Large language models (LLMs) and autonomous coding agents are increasingly used to generate software across a wide range of unmet domains.<n>Existing benchmarks and evaluations for secure code generation fall short-many measure only vulnerability reduction, disregard correctness preservation, or evaluate security and functionality on separate datasets.<n>We present GAUGE, the first fully automated benchmarking framework designed to rigorously evaluate the security and correctness of LLM-generated code in unison.
  arXiv  Detail & Related papers  (2025-11-24T22:26:14Z)
• Towards Robust Agentic CUDA Kernel Benchmarking, Verification, and Optimization [25.135006275638172]
  We introduce robust-kbench, a new benchmark for rigorous evaluation of kernel performance and correctness across varied scenarios.<n>We also present a comprehensive agentic framework that translates torch code to kernels and iteratively improve their runtime setting.<n>Our approach produces kernels outperforming torch implementations for practical applications, including forward and backward passes.
  arXiv  Detail & Related papers  (2025-09-16T11:08:30Z)
• AttestLLM: Efficient Attestation Framework for Billion-scale On-device LLMs [19.00344718051438]
  We present AttestLLM, the first-of-its-kind attestation framework to protect the hardware-level intellectual property (IP) of device vendors.<n>We show that AttestLLM enforces model legitimacy and exhibits resilience against model forgery and attacks.
  arXiv  Detail & Related papers  (2025-09-08T04:17:02Z)
• A Mixture of Linear Corrections Generates Secure Code [20.94236753015922]
  Large language models (LLMs) have become proficient at sophisticated code-generation tasks, yet remain ineffective at reliably detecting or avoiding code vulnerabilities.<n>We find that current LLMs encode precise internal representations that distinguish vulnerable from secure code.<n>We develop an inference-time steering technique that subtly modulates the model's token-generation probabilities through a mixture of corrections.
  arXiv  Detail & Related papers  (2025-07-13T06:27:33Z)
• VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
  Large language models (LLMs) are increasingly integrated in software development.<n> Ensuring correctness in LLM-generated code remains challenging.<n>Verifiable code generation offers a promising path to address this limitation.
  arXiv  Detail & Related papers  (2025-05-29T06:12:52Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)
• TOPLOC: A Locality Sensitive Hashing Scheme for Trustless Verifiable Inference [7.103455333148043]
  Large language models (LLMs) have proven to be very capable, but access to frontier models currently relies on inference providers.<n>We propose TOPLOC, a novel method for verifiable inference that addresses this problem.
  arXiv  Detail & Related papers  (2025-01-27T12:46:45Z)
• DSTC: Direct Preference Learning with Only Self-Generated Tests and Code to Improve Code LMs [56.4979142807426]
  We introduce underlinetextbfDirect Preference Learning with Only underlinetextbfSelf-Generated underlinetextbfTests and underlinetextbfCode (DSTC)<n>DSTC uses only self-generated code snippets and tests to construct reliable preference pairs.
  arXiv  Detail & Related papers  (2024-11-20T02:03:16Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.