Show HN: Cuq – Formal Verification of Rust GPU Kernels
6 months ago
- #formal verification
- #Rust
- #GPU programming
- Cuq is a framework for formally verifying the semantics of Rust GPU kernels by translating Rust's MIR into Coq and connecting it to the PTX memory model.
- No formal semantics currently exist for Rust GPU code, despite its ability to compile to PTX or SPIR-V.
- The project aims to define a mechanized operational semantics for a subset of MIR and prove memory-model soundness when compiled to PTX.
- Key goals include verifying kernel-level properties like absence of divergent barrier synchronization and conformance to the PTX consistency model.
- The framework provides a prototype toolchain for translating Rust-CUDA kernels into Coq terms and interfacing with PTX proofs.
- Future extensions may incorporate Rust's ownership and lifetime reasoning for end-to-end proofs of safety and correctness.