> ## Documentation Index
> Fetch the complete documentation index at: https://docs.theformalera.com/llms.txt
> Use this file to discover all available pages before exploring further.

# Fix a failure

> Read a counterexample, reproduce it on the GPU, and confirm the fix.

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

**1. Explain**

```bash theme={"system"}
theformalera explain F-0001
```

```text theme={"system"}
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.

**2. Reproduce on the GPU (optional)**

```bash theme={"system"}
theformalera repro F-0001 -o repro.py
python repro.py
```

```text theme={"system"}
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).

**3. Fix**

```diff theme={"system"}
-    n_pages = seq_len // PAGE_SIZE
+    n_pages = tl.cdiv(seq_len, PAGE_SIZE)
```

**4. Re-verify the file**

```bash theme={"system"}
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

> [accordion] 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:
>
> ```text theme={"system"}
> 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.

> [accordion] UNSAFE: out-of-bounds access or a race
>
> ```text theme={"system"}
> 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
> ```
>
> ```text theme={"system"}
> 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.

> [accordion] OVERFLOW: an index wraps or a float becomes infinite
>
> ```text theme={"system"}
> 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.

> [accordion] 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`.

> [accordion] 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:

```bash theme={"system"}
theformalera verify kernels/attn_decode.py --format json | jq '.results[] | {kernel, kind, detail, stuck_at}'
```

You then have three options:

1. **Rewrite** the kernel in a pattern the engine proves (see [Limitations](https://docs.theformalera.com/concepts/limitations.md)). `theformalera lemma search --key <spec key>` lists the patterns existing lemmas already cover.
2. **Waive** it with an owner and an expiry date (see [Policy and waivers](https://docs.theformalera.com/guides/policy-and-waivers.md)).
3. **Wait**: the nightly run retries UNKNOWN results when new lemmas for their node appear.

## Use a counterexample in your own tests

```python theme={"system"}
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.


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.