Show HN: Cuq – Formal Verification of Rust GPU Kernels

Hi all, this is a small research prototype I built that connects Rust's MIR (Mid-level IR) to Coq, the proof assistant used for formal verification.

cuq takes the MIR dump of a Rust CUDA kernel and translates it into a minimal Coq semantics that emits memory events, which are then lined up with the PTX memory model formalized by Lustig et al., ASPLOS 2019.

Right now it supports:

* a simple saxpy kernel (no atomics)

* an atomic flag kernel using acquire/release semantics

* a "negative" kernel that fails type/order checking

The goal isn't a full verified compiler yet. It's a first step toward formally checking the safety of GPU kernels written in Rust (e.g. correct use of atomics, barriers, and memory scopes).

Happy to hear thoughts from folks working in Rust verification, GPU compilers, or Coq tooling.

Do you think it might be easier to target cuTile instead of PTX? (Probably not, since it has a less formalized model?)