Cover Image

ProofWright: Towards Agentic Formal Verification of CUDA

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Chatterjee, Bodhisatwa, Zagieboylo, Drew, Damani, Sana, Hari, Siva, Kozyrakis, Christos
Format:	Preprint
Published:	2025
Subjects:	Software Engineering
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Hunting CUDA Bugs at Scale with cuFuzz
by: ziad, Mohamed Tarek Ibn, et al.
Published: (2026)

Towards Robust Agentic CUDA Kernel Benchmarking, Verification, and Optimization
by: Lange, Robert Tjarko, et al.
Published: (2025)

Phaedrus: Predicting Dynamic Application Behavior with Lightweight Generative Models and LLMs
by: Chatterjee, Bodhisatwa, et al.
Published: (2024)

KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code
by: Liu, Yuwei, et al.
Published: (2026)

Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications
by: Tagliaferro, Alberto, et al.
Published: (2026)

Agentic Verification of Software Systems
by: Tu, Haoxin, et al.
Published: (2025)

Towards Automated Formal Verification of Backend Systems with LLMs
by: Xu, Kangping, et al.
Published: (2025)

Selene: Pioneering Automated Proof in Software Verification
by: Zhang, Lichen, et al.
Published: (2024)

Combining Tests and Proofs for Better Software Verification
by: Huang, Li, et al.
Published: (2026)

Lemma Discovery in Agentic Program Verification
by: Zhao, Huan, et al.
Published: (2026)

Formal Verification of Consistency for Systems with Redundant Controllers
by: Johansson, Bjarne, et al.
Published: (2024)

KernelBlaster: Continual Cross-Task CUDA Optimization via Memory-Augmented In-Context Reinforcement Learning
by: Dong, Kris Shengjun, et al.
Published: (2026)

Formal Verification of Ecosystem Restoration Requirements using UML and Alloy
by: Sousa, Tiago, et al.
Published: (2024)

Structural Abstraction and Selective Refinement for Formal Verification
by: Luckeneder, Christoph, et al.
Published: (2025)

Supporting Software Formal Verification with Large Language Models: An Experimental Study
by: Wang, Weiqi, et al.
Published: (2025)

Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)
by: Hähnle, Reiner, et al.
Published: (2025)

Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles
by: Faria, João Pascoal, et al.
Published: (2026)

Towards Agentic Test-Driven Quality Assurance for 6G Networks
by: Tranoris, Christos, et al.
Published: (2026)

Using LLMs to Facilitate Formal Verification of RTL
by: Orenes-Vera, Marcelo, et al.
Published: (2023)

A Formal Verification Approach to Safeguard Controller Variables from Single Event Upset
by: Ganesha, et al.
Published: (2025)

A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method
by: Ishii, Daisuke
Published: (2024)

Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
by: Bryant, Dustin, et al.
Published: (2025)

Towards Operation Proof Obligation Generation for VDM
by: Battle, Nick, et al.
Published: (2025)

Improving Efficiency of GPU Kernel Optimization Agents using a Domain-Specific Language and Speed-of-Light Guidance
by: Hari, Siva Kumar Sastry, et al.
Published: (2026)

SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification
by: Ma, Lezhi, et al.
Published: (2026)

Towards a DSL to Formalize Multimodal Requirements
by: Gomez-Vazquez, Marcos, et al.
Published: (2025)

Towards Bridging Formal Methods and Human Interpretability
by: Paul, Abhijit, et al.
Published: (2025)

Automating Formal Verification with Reinforcement Learning and Recursive Inference
by: Tan, Max
Published: (2026)

From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification
by: Erfan, Md, et al.
Published: (2026)

Towards the Coordination and Verification of Heterogeneous Systems with Data and Time
by: Kräuter, Tim, et al.
Published: (2025)

An Agentic Approach Towards Replication Package Quality Evaluation
by: Mbida, Maximilian Alexander Amougou, et al.
Published: (2026)

Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs
by: Corazza, Jan, et al.
Published: (2025)

Automated Repair of AI Code with Large Language Models and Formal Verification
by: Charalambous, Yiannis, et al.
Published: (2024)

Enhancing non-Perl bioinformatic applications with Perl: Building novel, component based applications using Object Orientation, PDL, Alien, FFI, Inline and OpenMP
by: Argyropoulos, Christos
Published: (2024)

Towards Detecting Prompt Knowledge Gaps for Improved LLM-guided Issue Resolution
by: Ehsani, Ramtin, et al.
Published: (2025)

Toward Agentic Software Project Management: A Vision and Roadmap
by: Assalaarachchi, Lakshana Iruni, et al.
Published: (2026)

Towards Systematic Specification and Verification of Fairness Requirements: A Position Paper
by: Ramadan, Qusai, et al.
Published: (2025)

Logic Mining from Process Logs: Towards Automated Specification and Verification
by: Klimek, Radoslaw, et al.
Published: (2025)

Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair
by: Wang, Hongshu, et al.
Published: (2026)

Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
by: Wojtak, Connor, et al.
Published: (2025)