Litmus 🧪
Your kernel test is green. That is not the same as your
kernel being correct. On this corpus, 88% of planted bugs
pass the test everyone runs — fixed power-of-two shapes,
torch.rand(), allclose(rtol=1e-2). Litmus catches
100% of them with 0% false positives.
interval + affine error bounds symbolic OOB / race checks targeted falsification no GPU
Everything below runs in this tab, under Pyodide — the bound engine, the Triton parser, the constraint solver and the CPU kernel surrogate are pure Python over numpy. Source · Corpus dataset
1 · Check a kernel
The safety analysis and shape-space derivation read the
source only — no execution, no GPU. Pick a spec to also get a
sound error bound. Annotate buffer sizes with
# litmus: buffer x_ptr = M*N for a checked out-of-bounds result.
2 · Corpus demo
Full pipeline on one of the 25 labelled kernels: bound → safety → targeted falsification, with the counterexample delta-debugged before it is shown.
Benchmark
| metric | (A) standard | (B) fuzzing+ | (C) Litmus |
|---|---|---|---|
| bug detection rate | 12% | 62% | 100% |
| detection, numerically observable bugs only | 14% | 71% | 100% |
| false positives on correct kernels | 0% | 0% | 0% |
| wall clock, whole corpus | 0.5s | 1.0s | 40.9s |
- 88% of planted bugs pass condition (A) (14 of 16).
- certified bound available for 92% of kernels; median tightness (bound / worst measured deviation) 1.27e+03x.
- median counterexample size 2 elements (max 40960).
- 2 of 16 planted bugs have no numerical signature at all; no output comparison can detect them at any shape or distribution.
Support map and limits
- elementwise — CERTIFIED: +,-,*,/ , max/min, exp/log/sqrt/rsqrt/tanh/sigmoid/erf over an interval domain
- rowwise_reduction — CERTIFIED: one level of sum/mean/max reduction with elementwise pre- and post-processing, plus the Norm composite (covers softmax, layernorm, rms-norm, row sums)
- tiled_matmul — CERTIFIED: one contraction of symbolic length K with an elementwise epilogue, including a distinct accumulator dtype
- unsupported — NOT CERTIFIED: chained contractions (attention: QK^T -> softmax -> PV), nested reductions, data-dependent control flow, atomics into shared accumulators, scan/sort primitives
Verification is always relative to a declared domain; outside it
nothing is claimed. Without z3 the constraint backend is a bounded
search, so SAT (a witness) is real while UNSAT only
means "no counterexample inside the box" — and results say which. Where no
bound exists, falsification runs against a heuristic tolerance, labelled
as such. ACCEPT is not a proof of correctness. Litmus does not
generate kernels.