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

# Release sign-off

> Coverage levels L1–L3, the signed release certificate, and the deployment gate.

The CI gate ensures every kernel that gets merged is correct. Sign-off answers a bigger question: is this whole inference system correct for this model? The answer is a coverage level, written into a signed certificate that your deployment pipeline checks.

## Coverage levels

| Level | What is established | How |
| - | - | - |
| **L1** Kernels | Every annotated kernel is equivalent to the spec node it declares | `theformalera verify` |
| **L2** Nodes | Every node of the compute graph is covered by at least one kernel that passed L1, or declared under `[trusted]` | `theformalera coverage` |
| **L3** Graph | The recorded launch sequence matches the graph: every launch is a verified kernel, and tensors flow between kernels with consistent shapes | `theformalera trace` + `theformalera signoff --trace` |

L1 and L2 are static and run on every PR. L3 needs one short run on the target hardware, once per release.

## Check node coverage

```bash theme={"system"}
theformalera coverage
```

```text theme={"system"}
• Qwen/Qwen3.8-27B@1.0: 6 of 21 nodes covered by verified kernels
  not covered: gdn.in_proj, gdn.conv, gdn.core, gdn.norm, gdn.out_proj, mlp.gate_up, mlp.down, mlp_residual,
attn.qkv_proj, attn.qk_norm, attn.rope, attn.core, attn.gate, attn.o_proj, final_norm
  declare nodes computed by trusted libraries under [trusted] nodes = [...]
  trusted external: embed, lm_head
```

A node is covered only when it is covered in **every** layer that has it. `layers[3..15].mlp.act` alone does not cover `mlp.act`.

## Record the launch sequence (L3)

```bash theme={"system"}
theformalera trace --matrix scenarios.yaml -o trace.json -- python serve.py --model Qwen/Qwen3.8-27B --dry-run
```

`trace` runs your program in-process with Triton's JIT launcher instrumented. For every launch it records the kernel, the grid, the constexprs, and the shape, stride, dtype and storage of every tensor argument. Host control flow differs between prefill, decode and mixed batches, so `scenarios.yaml` lists the scenarios to cover:

```yaml scenarios.yaml theme={"system"}
scenarios:
  - name: prefill
    args: [--prompt-len, "2048"]
  - name: decode
    args: [--decode-steps, "32"]
    env:
      BATCH: "8"
```

Each scenario runs the command with its extra `args` and `env`. Launches of CUDA/CUTLASS kernels from a PyTorch extension are recorded when the extension calls `theformalera.trace.record_launch(...)` (the C++ macro `THEFORMALERA_TRACE_LAUNCH`).

> [!NOTE]
>
> For host-side control flow, L3 is sampling of the listed scenarios, not proof. The certificate says so: `"host_control_flow": "scenario-based sampling (L3); kernels: proof"`.

## Sign off

```bash theme={"system"}
theformalera verify                                    # a whole-project run, not a subset
theformalera signoff --model Qwen/Qwen3.8-27B@1.0 --trace trace.json -o release.cert.json
```

```text theme={"system"}
1 private lemma(s) from your organisation's library are in the proofs' dependency closure and ship with the
release so the customer can re-check it:
  L-d07f2c
generated a signing key .theformalera/signing-key.pem (public key .theformalera/signing-key.pub)
coverage L1 · nodes 6/21 · 6 kernels · scenarios —
  L3: no trace given (L3 needs `--trace`)
  L2: not covered: gdn.in_proj, gdn.conv, gdn.core, gdn.norm, gdn.out_proj, mlp.gate_up, mlp.down, mlp_residual,
attn.qkv_proj, attn.qk_norm, attn.rope, attn.core, attn.gate, attn.o_proj, final_norm
  lemma closure: 1 lemma(s) (0 public · 1 org · 0 local) + built-ins of the spec package · proofs/lemmas/
✓ signed certificate -> release.cert.json  (proofs in proofs)
```

* `signoff` refuses to run after a partial `verify` (`verify kernels/x.py`, or `--changed-only`).
* Private lemmas from your org library are needed for the customer's re-check, so they ship with the proofs. `signoff` lists them and asks first; pass `--yes` in CI.
* The signing key is `--key`, else `$THEFORMALERA_SIGNING_KEY`, else `.theformalera/signing-key.pem`, which is generated if it is missing. Keep the release key in a secret store.
* Next to the certificate, `proofs/` holds every proof file and `proofs/lemmas/` the Lean sources of the lemma closure.

See [Certificate format](https://docs.theformalera.com/reference/certificate.md) for the full statement.

## Gate the deployment

```bash theme={"system"}
theformalera cert verify release.cert.json --require L3 --commit $GIT_SHA --pubkey release.pub
```

```text theme={"system"}
✓ certificate valid · Qwen/Qwen3.8-27B@1.0.0 · sm_90a · level L1 · 6 kernels
```

and, for a level the release does not reach:

```text theme={"system"}
✗ coverage level L1 is below the required L2
```

`cert verify` exits 0 only when:

1. the DSSE signature verifies with `--pubkey` (or `$THEFORMALERA_SIGNER_PUBKEY`);
2. the coverage level is at least `--require` (default `L3`);
3. with `--commit`, the certificate's subject is that git commit;
4. with `--proofs`, every proof file and the lemma closure match their digests in the certificate, and they all re-check with Lean, lemmas first.

## Delivering to a customer

When you deliver a disposable inference system, ship the certificate, `proofs/` and `proofs/lemmas/` with it. Your customer can re-check everything with the standard Lean 4 toolchain, without trusting you or us. See [Re-check proofs](https://docs.theformalera.com/guides/recheck-proofs.md).


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