Release commands

coverage

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

• 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

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

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 and Certificate format.

cert verify

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

✓ certificate valid · Qwen/Qwen3.8-27B@1.0.0 · sm_90a · level L1 · 6 kernels
✗ coverage level L1 is below the required L2

CLI

Configuration

Formats

coverage

trace

signoff

cert verify

​coverage

​trace

​signoff

​cert verify

coverage

trace

signoff

cert verify