Skip to main content
theformalera verify exits with status 1 when the policy in theformalera.toml fails, so CI blocks the merge.

​
Policy

theformalera.toml
​
"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.
​
list[glob]
default:"[]"
Files where BOUNDED is accepted even when require_level = "proof".
​
list[str]
default:"all kinds"
Which kinds fail the run. Leave out unknown to let undecided kernels through without waivers, which is not recommended.
​
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:
theformalera.toml
id, kernel, verdict, reason, owner and expires are required. A waived result shows as 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.
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:
theformalera.toml
They appear in the certificate’s trusted list as trusted external library (embed).