Fix a failure

A FAILED verdict always comes with concrete evidence. Use this workflow to go from the verdict to a fix.

Explain

theformalera explain F-0001

F-0001  COUNTEREXAMPLE  paged_decode_attention -> Qwen/Qwen3.8-27B@1.0:layers[*].attn.core
failing configs    1 of 1
witness (minimal)  B=1, seq_len=1           o[0, 0, 0]: kernel nan, spec -0.253953
witness (typical)  B=1, seq_len=17          o[0, 0, 0]: kernel -0.163625, spec -0.17983
correct only when  seq_len % 16 == 0
notes              swept seq_len = 1..64: 4 correct, 60 wrong

  suspect  kernels/attn_decode.py:39
           n_pages = seq_len // PAGE_SIZE      # expected: tl.cdiv(seq_len, PAGE_SIZE)

Read it from the bottom up. The suspect line is the expression the failure traces back to. correct only when explains why your tests passed: they used multiples of 16.

Reproduce on the GPU (optional)

theformalera repro F-0001 -o repro.py
python repro.py

max abs diff: 0.42601415461163633

The script rebuilds the exact input the engine found, from a seed and a few integers (tfe.load_case). It runs your kernel on the GPU and compares the output with the spec’s float64 reference interpreter (tfe.spec_eval). --witness minimal uses the smallest witness instead (max abs diff: nan here).

Fix

-    n_pages = seq_len // PAGE_SIZE
+    n_pages = tl.cdiv(seq_len, PAGE_SIZE)

Re-verify the file

theformalera verify kernels/attn_decode.py

The counterexample is gone. Here the verdict becomes UNKNOWN, because paged online-softmax attention is not provable yet. For a kernel the engine can prove, it becomes PASS · PROVED.

Reading each failure kind

COUNTEREXAMPLE: the kernel computes a different function

The witness shows one output element where the kernel and the spec disagree. If correct only when reads never (fails for every tested value), the formula itself is wrong, not an edge case:

F-0002  COUNTEREXAMPLE  rollout_0412_rmsnorm -> Qwen/Qwen3.8-27B@1.0:layers[*].input_norm
witness (minimal)  T=1                      y[0, 0]: kernel -0.0193751, spec 0.106854
correct only when  never (fails for every tested value)

  suspect  kernels/rl_rollouts.py:28
           tl.store(Y + row * stride_y + cols, x * tl.rsqrt(ms + eps) * w, mask=mask)

Here the weight is applied as w, but Qwen3.8’s spec says (1 + w). Run theformalera spec show <key> and compare the formula term by term.

UNSAFE: out-of-bounds access or a race

F-0003  UNSAFE  rollout_0977_rmsnorm -> Qwen/Qwen3.8-27B@1.0:layers[*].input_norm
witness (minimal)  T=1                      out-of-bounds access on `X` at element offset 5120 (program (0, 0,
                   0)): address outside the allocation

F-0008  UNSAFE  residual_overlapping_tiles -> Qwen/Qwen3.8-27B@1.0:layers[*].attn_residual
witness (minimal)  T=1                      write-write conflict on `Y` at element offset 960 (program (1, 0, 0)):
                   address already written by program 0

Usual causes: a missing or wrong mask= on a load or store, or tiles that overlap. A write-write conflict is a race: which value survives depends on the GPU’s schedule.

OVERFLOW: an index wraps or a float becomes infinite

F-0006  OVERFLOW  silu_mul_int32_index -> Qwen/Qwen3.8-27B@1.0:layers[*].mlp.act
witness            T=61682                  int32 overflow of `%g` for T=61682
correct only when  T <= 61681

row * (2 * I) is computed in int32 and wraps for long prefills. Cast the program id first: tl.program_id(0).to(tl.int64). For float overflow, the usual causes are exp without subtracting the max, or a half-precision intermediate.

VACUOUS: the assumptions cannot all hold

Check assume= and domain= together. For example, T % 16 == 0 with domain={"T": (1, 8)} leaves no valid T.

UNANNOTATED: a kernel has no annotation

Add @tfe.implements(...), or move the file outside [policy] require_annotation.

When the result is UNKNOWN

theformalera explain only covers failures. For UNKNOWN, read the detail and stuck_at fields of the JSON report:

theformalera verify kernels/attn_decode.py --format json | jq '.results[] | {kernel, kind, detail, stuck_at}'

You then have three options:

Rewrite the kernel in a pattern the engine proves (see Limitations). theformalera lemma search --key <spec key> lists the patterns existing lemmas already cover.
Waive it with an owner and an expiry date (see Policy and waivers).
Wait: the nightly run retries UNKNOWN results when new lemmas for their node appear.

Use a counterexample in your own tests

import theformalera as tfe

case = tfe.load_case("F-0001", witness="typical")      # kernel_args are torch tensors on the GPU
paged_decode_attention[case.grid](**case.kernel_args, D=256, G=6, PAGE=16)
ref = tfe.spec_eval(case.spec_key, **{k: case.spec_args[k] for k in ["q", "k", "v", "seq_lens"]})
assert (case.output("o") - ref).abs().max() < 1e-2

This turns the counterexample into a regression test for the shape your differential tests never covered.

Get started

Concepts

Guides

Model conformance

Case studies

Help

Reading each failure kind

When the result is UNKNOWN

Use a counterexample in your own tests

​Reading each failure kind

​When the result is UNKNOWN

​Use a counterexample in your own tests

Reading each failure kind

When the result is UNKNOWN

Use a counterexample in your own tests