Release sign-off

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

theformalera coverage

• 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)

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:

scenarios.yaml

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

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

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

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 for the full statement.

Gate the deployment

theformalera cert verify release.cert.json --require L3 --commit $GIT_SHA --pubkey release.pub

✓ certificate valid · Qwen/Qwen3.8-27B@1.0.0 · sm_90a · level L1 · 6 kernels

and, for a level the release does not reach:

✗ coverage level L1 is below the required L2

cert verify exits 0 only when:

the DSSE signature verifies with --pubkey (or $THEFORMALERA_SIGNER_PUBKEY);
the coverage level is at least --require (default L3);
with --commit, the certificate’s subject is that git commit;
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.

Get started

Concepts

Guides

Model conformance

Case studies

Help

Coverage levels

Check node coverage

Record the launch sequence (L3)

Sign off

Gate the deployment

Delivering to a customer

​Coverage levels

​Check node coverage

​Record the launch sequence (L3)

​Sign off

​Gate the deployment

​Delivering to a customer

Coverage levels

Check node coverage

Record the launch sequence (L3)

Sign off

Gate the deployment

Delivering to a customer