Show HN: Cuq – Formal Verification of Rust GPU Kernels (opens in new tab)

(github.com)

94 pointsnsomani8mo ago63 comments

63 comments

39 comments · 9 top-level

skrrtww8mo ago· 21 in thread

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.

lacker8mo ago

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.

thefz8mo ago

> They're renaming Coq, too, for the obvious reason.

Which is a perfectly legitimate name in French and the whole "issue" can be worked around by spelling cee-oh-queue.

3 more replies

pwdisswordfishy8mo ago

Meanwhile, nobody consulted the French when the bit was being named.

OneDeuxTriSeiGo8mo ago

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.

ironmagma8mo ago

There is a reason they renamed Coq to Rocq.

2 more replies

webdevver8mo ago

cuke - it's heaven in a can!

1 more reply

Aloisius8mo ago

I think I must pronounce cucumber differently than you.

I'd expect cuke, if pronounced like cucumber would be queueck or cuck depending on which cu in cucumber you're using.

However I pronounce CUDA koo-da so cuq would be pronounced perhaps like kook.

Dilettante_8mo ago

Maybe this surprises you, but some people have different sensibilities than you do.

thefz8mo ago

Not the whole world speaks English. "Chicago" speaks funny in Italian, rename the city because I am offended. See how ridiculous it sounds?

nsomaniOP8mo ago

Oh wow, honestly this caught me off guard - I've been pronouncing it "kook" in my head the whole time.

skrrtww8mo ago

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.

1 more reply

skavi8mo ago

It's your project, but with the current name I'd expect this thread to be duplicated any time the project is discussed.

kurtis_reed8mo ago

What's so bad about it?

kelseyfrog8mo ago

Take a seat in the chair

jonathrg8mo ago

It sounds like cuck.

7bit8mo ago

Yeah, coq is already bad, but cuq is the cherry on top of it. I don't like both.

tracker18mo ago

Like a similar thread... I always thought of "coq" as "co queue" in terms of as a word. "cuq" as "cook" with the cu as in "CUDA" etc.

antonvs8mo ago

You know you're spending too much time on dubious sites when ...

nvader8mo ago

Not really, unfortunately the word hovers in the comment sections of mainstream American political discourse.

1 more reply

7bit8mo ago

And your low-key judging people for porn consumption in 2025.

1 more reply

webdevver8mo ago

not at all - its perfectly logical

you are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier)

Hexigonz8mo ago· 6 in thread

This is pretty cool! Are you sure about the name...

NitpickLawyer8mo ago

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.

bitwize8mo ago

It's called Rocq now—for this reason.

1 more reply

ahallock8mo ago

Aren't we more mature than this? Granted, it's the first thing I thought of as well

7bit8mo ago

Can we instead please be mature about choosing a adequate sounding name?

hnuser1234568mo ago

Bonus points if it runs on UNIX

CaptainOfCoit8mo ago

I'm getting a ԃҽʝα ʋυ

nsomaniOP8mo ago· 2 in thread

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.

gaogao8mo ago

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

nsomaniOP8mo ago

That instinct is right. cuTile would be easier to parse but harder to reason about formally.

1 more reply

kaffekaka8mo ago· 1 in thread

As a swede I am reminded of the Honda Fitta.

Rendello8mo ago

Or Heinz's mayo-ketchup fusion, which had a funny translation in a local native language:

"This new sandwich spread, whatever it is, they call it Mayochup, In Cree, it means shit-face. lol"

https://www.cbc.ca/news/canada/sudbury/mayochup-cree-transla...

orliesaurus8mo ago

Reading through this thread, it seems the naming debate is taking up most of the oxygen, but the underlying technical goal behind the project is worth highlighting. Formal verification for GPU kernels could make massively parallel Rust code safer and more reliable as more workloads move onto GPUs. Race conditions and undefined behaviors in GPU programming are notoriously tricky to reason about;

HOWEVER, I'm curious whether a proof‑driven approach like this can scale beyond toy examples or specific hardware assumptions. If so, it might set a precedent for bringing formal methods to other low‑level domains too......

the_real_cher8mo ago

I wished this name had been reserved for some sort of monitoring software.

ModernMech8mo ago

Two step guide to naming programming languages.

Step 1: Make sure no other programming language has the name you want.

Step 2: Make sure the name you want isn't a slur or rude word in all the languages your audience will write in. Be sure to check misspellings and homophones.

Optional 3rd step is to make sure the name lends itself to a cute animal mascot. For this project, I dunno maybe a corner chair is the mascot.

heromal8mo ago

Cuck?

thrownawaysz8mo ago

'Yer a cuq, Harry

j / k navigate · click thread line to collapse

63 comments

39 comments · 9 top-level

skrrtww8mo ago· 21 in thread

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.

lacker8mo ago

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.

thefz8mo ago

> They're renaming Coq, too, for the obvious reason.

Which is a perfectly legitimate name in French and the whole "issue" can be worked around by spelling cee-oh-queue.

3 more replies

pwdisswordfishy8mo ago

Meanwhile, nobody consulted the French when the bit was being named.

OneDeuxTriSeiGo8mo ago

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.

ironmagma8mo ago

There is a reason they renamed Coq to Rocq.

2 more replies

webdevver8mo ago

cuke - it's heaven in a can!

1 more reply

Aloisius8mo ago

I think I must pronounce cucumber differently than you.

I'd expect cuke, if pronounced like cucumber would be queueck or cuck depending on which cu in cucumber you're using.

However I pronounce CUDA koo-da so cuq would be pronounced perhaps like kook.

Dilettante_8mo ago

Maybe this surprises you, but some people have different sensibilities than you do.

thefz8mo ago

Not the whole world speaks English. "Chicago" speaks funny in Italian, rename the city because I am offended. See how ridiculous it sounds?

nsomaniOP8mo ago

Oh wow, honestly this caught me off guard - I've been pronouncing it "kook" in my head the whole time.

skrrtww8mo ago

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.

1 more reply

skavi8mo ago

It's your project, but with the current name I'd expect this thread to be duplicated any time the project is discussed.

kurtis_reed8mo ago

What's so bad about it?

kelseyfrog8mo ago

Take a seat in the chair

jonathrg8mo ago

It sounds like cuck.

7bit8mo ago

Yeah, coq is already bad, but cuq is the cherry on top of it. I don't like both.

tracker18mo ago

Like a similar thread... I always thought of "coq" as "co queue" in terms of as a word. "cuq" as "cook" with the cu as in "CUDA" etc.

antonvs8mo ago

You know you're spending too much time on dubious sites when ...

nvader8mo ago

Not really, unfortunately the word hovers in the comment sections of mainstream American political discourse.

1 more reply

7bit8mo ago

And your low-key judging people for porn consumption in 2025.

1 more reply

webdevver8mo ago

not at all - its perfectly logical

you are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier)

Hexigonz8mo ago· 6 in thread

This is pretty cool! Are you sure about the name...

NitpickLawyer8mo ago

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.

bitwize8mo ago

It's called Rocq now—for this reason.

1 more reply

ahallock8mo ago

Aren't we more mature than this? Granted, it's the first thing I thought of as well

7bit8mo ago

Can we instead please be mature about choosing a adequate sounding name?

hnuser1234568mo ago

Bonus points if it runs on UNIX

CaptainOfCoit8mo ago

I'm getting a ԃҽʝα ʋυ

nsomaniOP8mo ago· 2 in thread

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.

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.

gaogao8mo ago

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

nsomaniOP8mo ago

That instinct is right. cuTile would be easier to parse but harder to reason about formally.

1 more reply

kaffekaka8mo ago· 1 in thread

As a swede I am reminded of the Honda Fitta.

Rendello8mo ago

Or Heinz's mayo-ketchup fusion, which had a funny translation in a local native language:

"This new sandwich spread, whatever it is, they call it Mayochup, In Cree, it means shit-face. lol"

https://www.cbc.ca/news/canada/sudbury/mayochup-cree-transla...

orliesaurus8mo ago

the_real_cher8mo ago

I wished this name had been reserved for some sort of monitoring software.

ModernMech8mo ago

Two step guide to naming programming languages.

Step 1: Make sure no other programming language has the name you want.

Step 2: Make sure the name you want isn't a slur or rude word in all the languages your audience will write in. Be sure to check misspellings and homophones.

Optional 3rd step is to make sure the name lends itself to a cute animal mascot. For this project, I dunno maybe a corner chair is the mascot.

heromal8mo ago

Cuck?

thrownawaysz8mo ago

'Yer a cuq, Harry

j / k navigate · click thread line to collapse