> ## 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.

# The tail-page bug random tests miss

> A paged decode attention kernel passes its differential tests and is wrong for 60 of 64 sequence lengths.

The kernel is paged decode attention for the 16 Gated Attention layers of Qwen3.8-27B: one program per (sequence, query head), keys and values read page by page through the block table (page size 16), with an online softmax. It counts pages like this:

```python kernels/attn_decode.py theme={"system"}
n_pages = seq_len // PAGE_SIZE
for p in range(0, n_pages):
    ...
```

It should round up. The tokens of a partial last page are never read.

## The differential test passes

Random bf16 inputs on an RTX 4090, compared with a float64 PyTorch reference at the conventional lengths:

```text theme={"system"}
$ python -m pytest -q -s tests/test_attn_decode.py
seq_len=  128  max abs diff 1.38e-07
.seq_len=  512  max abs diff 8.52e-08
.seq_len= 1024  max abs diff 1.11e-07
.seq_len= 2048  max abs diff 6.36e-08
.
4 passed in 1.95s
```

![pytest output: four differential tests pass at sequence lengths 128, 512, 1024 and 2048](https://mintcdn.com/n-a-24de7f09/RKvaTncjzKh3Uq1K/images/screenshots/case1-differential-test-passes.png?fit=max\&auto=format\&n=RKvaTncjzKh3Uq1K\&q=85\&s=47d989bcb32c3c95356e68636cd8a929)

Every length is a multiple of 16, so the bug never triggers. Other lengths do trigger it: `seq_len = 1` gives NaN, `17` gives an error of 0.73, `100` gives 0.20. And `seq_len = 2047` still passes `allclose`: one missing token in 2047 stays inside the tolerance.

## The verifier rejects it, on a CPU, in 2.5 s

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

![theformalera verify reports FAILED F-0001, and explain shows the witnesses, the failing region seq\_len % 16 == 0 and the suspect line](https://mintcdn.com/n-a-24de7f09/RKvaTncjzKh3Uq1K/images/screenshots/case1-theformalera-counterexample.png?fit=max\&auto=format\&n=RKvaTncjzKh3Uq1K\&q=85\&s=7ba9d88625aa23e5ca8923ebdad00506)

`correct only when seq_len % 16 == 0` explains why the tests passed. The suspect line names the expression to change and the expected one.

## And the repro confirms it on the GPU

```text theme={"system"}
$ theformalera repro F-0001 -o repro.py && python repro.py
max abs diff: 0.42601415461163633
$ theformalera repro F-0001 --witness minimal -o repro_min.py && python repro_min.py
max abs diff: nan
```

![The generated repro script prints a max abs diff of 0.426 for seq\_len 17 and nan for seq\_len 1](https://mintcdn.com/n-a-24de7f09/RKvaTncjzKh3Uq1K/images/screenshots/case1-repro-on-gpu.png?fit=max\&auto=format\&n=RKvaTncjzKh3Uq1K\&q=85\&s=fc13a0dd07c7ccb12a92640a760dc32e)

## What to take away

* A test that samples inputs can only show the bug on the inputs it samples. The verifier searches the whole shape domain and reports the failing region.
* No GPU is needed to find the bug, only to look at it.
* After the fix (`tl.cdiv(seq_len, PAGE_SIZE)`) the counterexample is gone. The kernel is UNKNOWN rather than PROVED, because paged online-softmax proofs are not wired in yet. See [Limitations](https://docs.theformalera.com/concepts/limitations.md).


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