Verifying CUDA Kernels in Coq with Rust MIR (Introducing cuq)

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 ker…


This content originally appeared on DEV Community and was authored by Neel Somani

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

  1. MIR Extraction - cuq operates on Rust's Mid-level IR.
  2. MIR to Coq Translation — the compiler pass encodes MIR statements into Coq syntax.
  3. Integration with PTX Model — generated Coq files import the formal PTX semantics from Lustig et al.
  4. 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.

GitHub: https://github.com/neelsomani/cuq


This content originally appeared on DEV Community and was authored by Neel Somani


Print Share Comment Cite Upload Translate Updates
APA

Neel Somani | Sciencx (2025-10-23T01:51:00+00:00) Verifying CUDA Kernels in Coq with Rust MIR (Introducing cuq). Retrieved from https://www.scien.cx/2025/10/23/verifying-cuda-kernels-in-coq-with-rust-mir-introducing-cuq/

MLA
" » Verifying CUDA Kernels in Coq with Rust MIR (Introducing cuq)." Neel Somani | Sciencx - Thursday October 23, 2025, https://www.scien.cx/2025/10/23/verifying-cuda-kernels-in-coq-with-rust-mir-introducing-cuq/
HARVARD
Neel Somani | Sciencx Thursday October 23, 2025 » Verifying CUDA Kernels in Coq with Rust MIR (Introducing cuq)., viewed ,<https://www.scien.cx/2025/10/23/verifying-cuda-kernels-in-coq-with-rust-mir-introducing-cuq/>
VANCOUVER
Neel Somani | Sciencx - » Verifying CUDA Kernels in Coq with Rust MIR (Introducing cuq). [Internet]. [Accessed ]. Available from: https://www.scien.cx/2025/10/23/verifying-cuda-kernels-in-coq-with-rust-mir-introducing-cuq/
CHICAGO
" » Verifying CUDA Kernels in Coq with Rust MIR (Introducing cuq)." Neel Somani | Sciencx - Accessed . https://www.scien.cx/2025/10/23/verifying-cuda-kernels-in-coq-with-rust-mir-introducing-cuq/
IEEE
" » Verifying CUDA Kernels in Coq with Rust MIR (Introducing cuq)." Neel Somani | Sciencx [Online]. Available: https://www.scien.cx/2025/10/23/verifying-cuda-kernels-in-coq-with-rust-mir-introducing-cuq/. [Accessed: ]
rf:citation
» Verifying CUDA Kernels in Coq with Rust MIR (Introducing cuq) | Neel Somani | Sciencx | https://www.scien.cx/2025/10/23/verifying-cuda-kernels-in-coq-with-rust-mir-introducing-cuq/ |

Please log in to upload a file.



There are no updates yet.
Click the Upload button above to add an update.

You must be logged in to translate posts. Please log in or register.

Related Posts