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

# Policy and waivers

> Decide which verdicts fail CI, and record time-limited exceptions with an owner.

`theformalera verify` exits with status 1 when the policy in `theformalera.toml` fails, so CI blocks the merge.

## Policy

```toml theformalera.toml theme={"system"}
[policy]
require_level      = "proof"                     # BOUNDED fails unless the file matches allow_bounded_on
allow_bounded_on   = ["kernels/experimental/**"]
fail_on            = ["counterexample", "unsafe", "overflow", "vacuous", "unknown"]
require_annotation = ["kernels/**/*.py", "csrc/**/*.cu"]
```

**require\_level** `"proof" | "bounded"` (default: proof)

With `proof`, a `PASS · BOUNDED` result fails, unless the kernel's file matches `allow_bounded_on`. With `bounded`, both PASS subtypes pass.

**allow\_bounded\_on** `list[glob]` (default: \[])

Files where `BOUNDED` is accepted even when `require_level = "proof"`.

**fail\_on** `list[str]` (default: all kinds)

Which kinds fail the run. Leave out `unknown` to let undecided kernels through without waivers, which is not recommended.

**require\_annotation** `list[glob]` (default: \[])

Every `@triton.jit` kernel under these paths must be annotated, or called by an annotated launcher. A kernel that is never annotated is never verified, so without this setting an unannotated kernel can never fail CI.

## Waivers

A waiver accepts one verdict for one kernel, until a date:

```toml theformalera.toml theme={"system"}
[[waiver]]
id      = "W-1"
kernel  = "paged_decode_attention"     # fnmatch pattern on the kernel name
verdict = "unknown"                    # or a kind: unsupported, timeout, bounded, …
reason  = "paged online-softmax lemma pending; no counterexample, safety checks pass"
owner   = "alice"
expires = 2026-11-30
```

`id`, `kernel`, `verdict`, `reason`, `owner` and `expires` are required. A waived result shows as `waived`:

```text theme={"system"}
 paged_decode_attention   layers[*].attn.core            0/1   UNKNOWN   waived       cached

5 passed · 0 failed · 1 unknown · 1 waived
```

Rules:

* A waiver **expires**: from the day after `expires` it no longer applies, and the run fails with `waiver W-1 for paged_decode_attention expired on 2026-11-30`.
* **COUNTEREXAMPLE and UNSAFE** are confirmed bugs. Waiving one also needs `approved_by = "<org admin>"`, or the run fails with `waiver … cannot waive a confirmed bug … without approved_by`.
* Every active waiver is written into the [release certificate](https://docs.theformalera.com/reference/certificate.md).

When an UNKNOWN becomes PROVED on a later run (for example, after new lemmas arrive), the waiver simply stops matching. Remove it.

## Trusted nodes

Nodes computed by external libraries (cuBLAS for `lm_head`, `torch.nn.Embedding` for `embed`) have no annotated kernel. Declare them so that they count towards [L2 coverage](https://docs.theformalera.com/guides/release-signoff.md):

```toml theformalera.toml theme={"system"}
[trusted]
nodes = ["embed", "lm_head"]  # computed by cuBLAS / torch.nn.Embedding
```

They appear in the certificate's `trusted` list as `trusted external library (embed)`.


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