We were talking the other day about the lack of formal verification of FlashAttention 3, which, it was pointed out to me, somewhat undersells the tremendous amount of verification work going on for kernels right now. Fair!
When OpenAI announced their Jalapeño chip a couple of months back, SemiAnalysis went along to take a look at what they had done. OAI showed off some kernels, written by Codex, for getting DeepSeek MLA running on the chip. As Jordan Nanos of SA put it:
“The point is, the guys who were scrolling through this code with us, it was kind of clear that they know a whole bunch about hardware, they know a whole bunch about the concepts in the system, and they just have no idea what this MLA kernel that they’re showing us for DeepSeek actually does.”
They didn’t have to read it because they were confident it was correct. Which is not a particularly easy thing to do. A new paper from Microsoft Research and friends, RESOLVE, had 5.6 Sol write optimized versions of the 100 level 1 KernelBench problems, looping until each passed the benchmark’s tolerance checks. Two of them, an ELU and a hardtanh, were… empty. They literally didn’t do anything, and passed anyway
The decision of what you are actually verifying is quite a consequential one. Even for something as straightforward as “accuracy”, choosing a tolerance for torch.allclose changes the design space. From the RESOLVE paper:
Testing must consequently compare outputs using a numerical tolerance, but a permissive tolerance can conceal bugs while a restrictive one can reject valid optimizations.
Even if you lock down your numerics, you still have a range of inputs and execution conditions. The TIRx Harness is an agentic-oriented stack of compiler+tools for exactly this kind of kernel loop<sup>2</sup>, and made a special effort around verifying concurrency:
In one KDA trace, a candidate passed the benchmark’s correctness tests, but synchronization analysis still identified a latent bug: a reused mbarrier could advance to its next generation before a late consumer finished waiting on the previous one.
The RESOLVE folks attempt to prove their kernels are correct<sup>3</sup> using Kuiper, a verification language that compiles down to CUDA. WarpDRF, another Tyler Sorensen joint, looked at warp primitives like shuffles, tensor core ops, warp barriers. Which threads take part in different operations depends on how the threads diverge. They used Rocq, another verifier language, to prove they were consistent, then fuzzed thousands of test per config across a range of devices to see if they held.
Most of it held together, but Nvidia was… patchy. If the whole warp stays together, you are good. Beyond that, you just don’t know which threads are going to participate. The team used their findings to build a static checker and ran it over the kernels in llama.cpp. Most of the kernels were fine, but a few weren’t!
Zhongming Yu, one of the authors of NVIDIA’s CAKE, wrote a compelling post the other day talking about how the blocker for true recursive self improvement is the speed of verification, and specifically called out megakernels as an example of fragile workloads. Kernels generally run pretty quickly (hence why we can autotune), but setting up the right verification is hard, and the more complex the verification, the slower the whole loop goes.
RESOLVE costs it out, towards the end of the paper. Testing elementwise ops took milliseconds. Determinism testing took about 1.5 minutes per kernel. Reduction and concurrency… around 2.4 hours.
- And, this wasn’t even surprising! KernelBench’s maintainers list no-op kernels as a common reward hack: if the output buffer still holds the answer from an earlier run, doing nothing is very fast and very correct.↩︎
- As an aside in the more questionably-verification side, one agent found an output-lane masking option on
tcgen05.mmaby reading the ISA, which is cool. It didn’t reduce the work at all, but did raise the observed clock frequency, for a 2-3% win. Would be interesting to see if that one holds up outside the benchmark - They have a reference kernel and an optimized one, and they are proving equivalence. They create a simplified version of each with minimal concurrency, ensure they generates the same answers, then validate the kernels are equivalent using Kuiper. ↩︎