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

# Verdicts

> PASS, FAILED and UNKNOWN, their subtypes, and what CI does with each.

Every (kernel, Spec Key) pair gets one verdict. When a kernel has several constexpr configurations, each is verified on its own and the kernel gets the worst of them.

| Verdict | Subtype | Meaning | CI by default |
| - | - | - | - |
| PASS | `PROVED` | Proved for the whole shape domain; the Lean 4 kernel checked the proof | passes |
| PASS | `BOUNDED` | Proved only for an enumerated set of shapes; one Lean 4 proof per shape | fails when `require_level = "proof"`, unless the file matches `allow_bounded_on` |
| FAILED | `COUNTEREXAMPLE` | Not equivalent to the spec; a concrete input is attached | fails |
| FAILED | `UNSAFE` | Out-of-bounds access, a write-write conflict between programs, or an output element never written | fails |
| FAILED | `OVERFLOW` | An index can wrap, or a float intermediate can become infinite, inside the declared domain | fails |
| FAILED | `VACUOUS` | The assumptions contradict each other, so any proof would be empty | fails |
| FAILED | `UNANNOTATED` | A kernel under `require_annotation` has no annotation | fails |
| UNKNOWN | `UNSUPPORTED` | The engine reached a construct it cannot prove yet; the stuck IR location is reported | fails; waivable |
| UNKNOWN | `TIMEOUT` | The Lean check exceeded the time budget | fails; waivable |

> [!WARNING]
>
> **UNKNOWN is never a PASS.** When the engine cannot decide, it says so. One false PASS would destroy the value of every other one.

## Order of precedence

When configurations disagree, the kernel's verdict is the first match in this order:

`COUNTEREXAMPLE` → `UNSAFE` → `OVERFLOW` → `VACUOUS` → `TIMEOUT` → `UNSUPPORTED` → `BOUNDED` → `PROVED`

In the `configs` column of the terminal table, `4/4` means four of four configurations passed, and `0/1` means the only one failed.

## Failure ids

Every FAILED pair gets a stable id such as `F-0001`. The same (file, kernel, Spec Key, kind) keeps its id across runs. Use the id with:

* `theformalera explain F-0001`: witnesses, failing region, suspect line;
* `theformalera repro F-0001 -o repro.py`: a PyTorch script that runs the kernel on the GPU with that input;
* `tfe.load_case("F-0001")` in your own tests.

## What a FAILED verdict tells you

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

| Field | Meaning |
| - | - |
| `witness (minimal)` | The smallest failing input found |
| `witness (typical)` | A failing input of ordinary size, closer to what tests use |
| `correct only when` | The engine's description of the region where the kernel is still right. It tells you which inputs are safe, and why your tests passed. |
| `suspect` | The source line whose expression the failure traces back to, with the expected expression when the engine can tell |
| `notes` | For example, `swept seq_len = 1..64: 4 correct, 60 wrong` |

## Levels

`--level` (or `[verify] level`) sets how hard the engine tries:

| Level | Counterexample search | Proof | Use |
| - | - | - | - |
| `proof` | Up to 12 shapes per config | Full Lean 4 proof, then bounded fallback | CI, release |
| `bounded` | Same as `proof` | Same as `proof` | reserved; behaves like `proof` in this release |
| `quick` | Up to 4 small shapes | Full proof, no bounded fallback | pre-commit, agents' inner loop |

Whether a `BOUNDED` result passes is decided by the policy, not by the level: set `[policy] require_level = "bounded"`, or list the files under `allow_bounded_on`.

## Cached results

Results are cached by lowered-IR hash, spec hash, engine version, assumptions and binding. Changing only comments or formatting does not change the IR, so it does not trigger a new proof. The `time` column then shows `cached`.

PASS and FAILED never depend on the lemma library, so they are never recomputed. An UNKNOWN records the lemmas it was tried with, and is retried when new lemmas for its node appear.


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