Release certificate

A release certificate is an in-toto Statement, wrapped in a DSSE envelope and signed with Ed25519.

The envelope

release.cert.json

{
  "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):

{
  "_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

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.

CLI

Configuration

Formats

The envelope

The statement

Predicate fields

Shipped files

​The envelope

​The statement

​Predicate fields

​Shipped files

The envelope

The statement

Predicate fields

Shipped files