Overview
GPU kernels are notoriously difficult to reason about formally. While prior work such as Lustig et al. (ASPLOS 2019) defined a Coq model of the PTX memory semantics, there has not been a practical toolchain connecting high-level kernel code to verifiable proofs.
cuq is an experimental Rust-to-Coq pipeline that lets you write CUDA kernels in safe Rust and automatically generate Coq representations of their execution traces. Each MIR instruction is translated into Coq terms compatible with the PTX memory model, allowing proofs of correctness and safety properties.
Architecture
- MIR Extraction – cuq operates on Rust’s Mid-level IR.
- MIR to Coq Translation — the compiler pass encodes MIR statements into Coq syntax.
- Integration with PTX Model — generated Coq files import the formal PTX semantics from Lustig et al.
- Verification — developers can reason about kernel safety and memory consistency directly in Coq.
Significance
By connecting Rust’s ownership and type guarantees with Coq’s formal proof system, cuq provides a foundation for provably safe GPU programming. It demonstrates that performance-oriented languages and proof-based verification can coexist in a single toolchain.