Verdicts

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

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

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.

Get started

Concepts

Guides

Model conformance

Case studies

Help

Order of precedence

Failure ids

What a FAILED verdict tells you

Levels

Cached results

​Order of precedence

​Failure ids

​What a FAILED verdict tells you

​Levels

​Cached results

Order of precedence

Failure ids

What a FAILED verdict tells you

Levels

Cached results