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

> The signed in-toto statement that theformalera signoff produces and cert verify checks.

A release certificate is an [in-toto](https://in-toto.io) Statement, wrapped in a [DSSE](https://github.com/secure-systems-lab/dsse) envelope and signed with Ed25519.

## The envelope

```json release.cert.json theme={"system"}
{
  "payloadType": "application/vnd.in-toto+json",
  "payload": "<base64 of the statement>",
  "signatures": [ { "keyid": "ed25519:597c2a2afdb151fe10a3367a5ab540b8", "sig": "<base64>" } ]
}
```

The signature covers the DSSE pre-authentication encoding of `payloadType` and the payload.

## The statement

A real statement (kernels trimmed to one):

```json theme={"system"}
{
  "_type": "https://in-toto.io/Statement/v1",
  "subject": [ { "name": "acme-qwen3.8-27b-h100", "digest": { "gitCommit": "1b428c81c9de11c4541ddd741114f8686f76d2fe" } } ],
  "predicateType": "https://theformalera.com/attestation/signoff/v1",
  "predicate": {
    "model": "Qwen/Qwen3.8-27B@1.0.0",
    "spec_digest": "sha256:313a42af237f0db7ec729fd0d5d9230d932d829da0cbda0c43bdb4d310aaddf4",
    "lock_digest": "sha256:7f03268e42f81adf8a710cc7d626057d9b083243a4fb27f52d818c47fe0606bf",
    "hardware": "sm_90a",
    "issued": "2026-11-01T04:11:06+00:00",
    "coverage": {
      "level": "L1",
      "nodes": "6/21",
      "scenarios": [],
      "host_control_flow": "scenario-based sampling (L3); kernels: proof"
    },
    "kernels": [
      {
        "name": "silu_mul_kernel",
        "file": "kernels/act.py",
        "node": "layers[*].mlp.act",
        "verdict": "PROVED",
        "ir": ["sha256:1894967eb9b8d719945be4d639ed96c91fd7d00d24c17903107b84128b7072fb"],
        "proof": "proofs/silu_mul_kernel__layers____mlp_act__b127356f45.lean",
        "proof_digest": "sha256:9df0c5ee960dc05c4d235ef4e80d732d86e5ed2f0ee698d136247898d1fe079d",
        "configs": [
          {
            "config": { "BLOCK": 1024, "I": 17408 },
            "ir": "sha256:1894967eb9b8d719945be4d639ed96c91fd7d00d24c17903107b84128b7072fb",
            "proof": "proofs/silu_mul_kernel__layers____mlp_act__b127356f45.lean",
            "proof_digest": "sha256:9df0c5ee960dc05c4d235ef4e80d732d86e5ed2f0ee698d136247898d1fe079d"
          }
        ]
      }
    ],
    "lemmas": {
      "count": 1, "public": 0, "org": 1, "local": 0, "builtin_hits": 0,
      "ids": ["L-d07f2c"], "private_ids": ["L-d07f2c"],
      "closure": "proofs/lemmas/",
      "digest": "sha256:43c2026fc734a4cf07e120cb1d0affbd37344cb658784bb2bf25b9fdc61c7885"
    },
    "assumptions": ["contiguous(Hh)", "contiguous(X)", "contiguous(Y)"],
    "waivers": [
      { "id": "W-1", "owner": "alice", "expires": "2026-11-30",
        "reason": "paged online-softmax lemma pending; no counterexample, safety checks pass" }
    ],
    "trusted": ["Lean 4 kernel", "IR-to-Lean translation", "triton frontend", "ptxas",
                "trusted external library (embed)", "trusted external library (lm_head)"],
    "engine": "theformalera engine 2026.10",
    "cli": "theformalera 0.9.0"
  }
}
```

## Predicate fields

| Field | Meaning |
| - | - |
| `model` | Model key and the exact locked spec version |
| `spec_digest`, `lock_digest` | The spec package and the lock the release was verified against |
| `hardware` | Target architecture |
| `coverage.level` | `L1`, `L2`, `L3`, or `none` |
| `coverage.nodes` | Covered / total graph nodes (trusted nodes count as covered) |
| `coverage.scenarios` | Traced scenarios, for L3 |
| `kernels[]` | Per kernel: node, verdict, IR digests, and the proof file with its SHA-256 for every configuration |
| `lemmas` | The lemma dependency closure: ids by library, which ones are private, where the Lean sources are, and their digest |
| `assumptions` | Every assumption the proofs rely on |
| `waivers` | Every waiver that was active |
| `trusted` | The trusted base, including declared external libraries |

The Lemma Hub is deliberately not in `trusted`: its lemmas ship as Lean source and are checked again on every re-check.

## Shipped files

```text theme={"system"}
release.cert.json
proofs/
  silu_mul_kernel__layers____mlp_act__b127356f45.lean
  rmsnorm_kernel__layers____input_norm__9d6f70d2a5.lean
  …
  lemmas/
    TFELemmas/Pack_ebb6fde7c219.lean
```

`theformalera cert verify --proofs` checks the signature, the level, the commit, and every proof file and the lemma closure against their digests. It then re-checks them all with Lean. See [Release sign-off](https://docs.theformalera.com/guides/release-signoff.md#gate-the-deployment).


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