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

> coverage, trace, signoff and cert verify.

## coverage

```bash theme={"system"}
theformalera coverage [--json]
```

L2 coverage from the last run: for each locked model, the graph nodes covered by a passing kernel in every layer that has them, the uncovered ones, and the nodes declared under `[trusted]`.

```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
```

`--json` prints `{model: {covered, total, uncovered, partial, trusted}}`. `partial` lists nodes covered in some layers but not all.

## trace

```bash theme={"system"}
theformalera trace [-o trace.json] [--matrix scenarios.yaml] -- python serve.py [ARGS]...
```

Run a Python program in-process with Triton's JIT launcher instrumented, and record every launch: kernel, module, grid, constexprs, scalar arguments, and the shape, stride, dtype, storage pointer and offset of every tensor argument.

| Option | Default | Meaning |
| - | - | - |
| `-o` | `trace.json` | Output file (`theformalera.trace/v1`) |
| `--matrix` | — | A YAML or JSON list of scenarios `{name, args, env}`; the program runs once per scenario |

Everything after `--` is the program: `python script.py …` or `python -m module …`. Tracing never changes the program's behaviour; a launch the recorder cannot parse is skipped.

## signoff

```bash theme={"system"}
theformalera signoff --model KEY@VERSION [--trace trace.json] [-o release.cert.json] [--key key.pem]
                     [--hardware sm_90a] [--yes]
```

Build the in-toto release statement from the last **whole-project** run, sign it, and copy the proofs and the lemma closure next to it (`proofs/`, `proofs/lemmas/`).

| Option | Default | Meaning |
| - | - | - |
| `--model` | required | Model and spec version, for example `Qwen/Qwen3.8-27B@1.0` |
| `--trace` | — | A launch trace; needed for L3 |
| `-o` | `release.cert.json` | Certificate file (a DSSE envelope) |
| `--key` | `$THEFORMALERA_SIGNING_KEY`, else `.theformalera/signing-key.pem` (generated if missing) | Ed25519 signing key (PEM) |
| `--hardware` | the first `[targets] triton arch` | Target hardware recorded in the certificate |
| `--yes` | off | Confirm shipping private org-library lemmas with the proofs |

See [Release sign-off](https://docs.theformalera.com/guides/release-signoff.md) and [Certificate format](https://docs.theformalera.com/reference/certificate.md).

## cert verify

```bash theme={"system"}
theformalera cert verify CERT [--require L1|L2|L3] [--commit SHA] [--pubkey key.pub] [--proofs]
```

The deployment gate. Exit 0 only if the certificate is valid for the requirement.

| Option | Default | Meaning |
| - | - | - |
| `--require` | `L3` | Minimum coverage level |
| `--commit` | — | The git commit the release must be built from (prefix match) |
| `--pubkey` | `$THEFORMALERA_SIGNER_PUBKEY` | Signer's public key (PEM); required |
| `--proofs` | off | Also check every proof file and the lemma closure against their digests, then re-check them all with Lean |

```text theme={"system"}
✓ certificate valid · Qwen/Qwen3.8-27B@1.0.0 · sm_90a · level L1 · 6 kernels
✗ coverage level L1 is below the required L2
```


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