[HN Gopher] Show HN: Cuq - Formal Verification of Rust GPU Kernels
___________________________________________________________________
Show HN: Cuq - Formal Verification of Rust GPU Kernels
Author : nsomani
Score : 25 points
Date : 2025-10-22 19:38 UTC (3 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| nsomani wrote:
| 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.
| gaogao wrote:
| Do you think it might be easier to target cuTile instead of
| PTX? (Probably not, since it has a less formalized model?)
| nsomani wrote:
| That instinct is right. cuTile would be easier to parse but
| harder to reason about formally.
| Hexigonz wrote:
| This is pretty cool! Are you sure about the name...
| NitpickLawyer wrote:
| It's a system where a 3rd party library (aptly named Coq) gets
| to _throughly_ verify your kernel, and you get to watch it do
| its thing? I think the name is fitting.
| bitwize wrote:
| It's called Rocq now--for this reason.
| sayrer wrote:
| Yeah, "coq" is a grade school joke in French class. It just
| means "rooster" or something in French, but it sounds
| ridiculous in English. This one has the same problem.
|
| A company with that in the name made the French national
| team jersey for a while.
|
| https://en.wikipedia.org/wiki/Le_Coq_Sportif
|
| It's Nike now, but it still has a rooster on it.
| CaptainOfCoit wrote:
| I'm getting a [?]chja vu
| hnuser123456 wrote:
| Bonus points if it runs on UNIX
| skrrtww wrote:
| This might be the worst named project of all time. Not funny and
| demonstrates an absolutely terrible impulse on the part of the
| author. Probably the worst way possible to advertise your
| project.
|
| edit: According to the author in a reply, the double entendre was
| in fact not intentional.
| Dilettante_ wrote:
| Maybe this surprises you, but some people have different
| sensibilities than you do.
| webdevver wrote:
| not at all - its perfectly logical
|
| you are cucking the betabuxxed bugs in your kernels with your
| BFV (Big Formal Verifier)
| nsomani wrote:
| Oh wow, honestly this caught me off guard - I've been
| pronouncing it "kook" in my head the whole time.
| skrrtww wrote:
| If this was genuinely unintentional on your part, then bless
| your heart and I'm sorry for assuming the worst. You might be
| the least morally corrupted internet user alive today.
| nsomani wrote:
| I think I've just spent too much time reading the word
| "CUDA" that I read "cu" as "koo", lol.
| OneDeuxTriSeiGo wrote:
| That's not what the name is based on. The name is cu- (as in
| CUDA kernels) -q (as in coq/rocq). Pronounced Cuke like
| cucumber.
| webdevver wrote:
| cuke - it's heaven in a can!
| lacker wrote:
| They're renaming Coq, too, for the obvious reason.
|
| Just go ahead and rename this project to "Rocuda", save
| everyone a lot of time arguing about what names are appropriate
| or not.
| thrownawaysz wrote:
| 'Yer a cuq, Harry
___________________________________________________________________
(page generated 2025-10-22 23:00 UTC)