Someone built a formal verifier for LLM-written CUDA code
A new tool checks if ChatGPT's GPU kernels are actually correct before you run them in production.
Read the note 1 min read
From the notebook
formal-verification.
2 notes on this topic.
From the notebook
2 notes on this topic.
A new tool checks if ChatGPT's GPU kernels are actually correct before you run them in production.
Turso used a TLA+ variant called Quint to model their libSQL fork and found over ten real bugs in SQLite's transaction logic that billions of existing tests never saw.