Cuqは、Rustで書かれたGPUカーネルを形式的に検証するためのフレームワークです。Rustはシステム言語としての地位を確立しつつあり、Rust-CUDAやrust-gpuなどのプロジェクトを通じてGPUプログラミングに進出しています。しかし、RustのGPUサブセットに関する形式的セマンティクスは存在せず、Rustのコンパイラの中間表現（MIR）からNVIDIAのPTXへの正確なマッピングも確立されていません。Cuqは、MIRをCoqに変換し、PTXのメモリモデルに接続することで、Rust GPUカーネルのセマンティクスを形式的に検証する初のフレームワークを提供します。MIRは、Rustの制御フローや副作用情報を保ったまま、構文を排除した型安全な中間表現です。この技術アプローチでは、MIRの機械的なセマンティクスを定義し、MIRからCoqへの変換ツールを開発することが目指されています。最終的には、MIRカーネルがデータ競合のない状態で、PTXメモリモデルに一貫した実行を許すことを証明することが目指されています。