Reports

Every form of output is rendered from the same objects, so a verdict reads the same in the terminal, in JSON, in SARIF and in the PR comment.

theformalera verify --report-dir .theformalera/report     # all four files
theformalera verify --format json                          # the run report on stdout
theformalera verify --sarif results.sarif                  # SARIF only

File	Contents
`theformalera-report.json`	The run report (`theformalera.run/v1`)
`theformalera.sarif`	SARIF 2.1.0, for code-scanning line annotations
`theformalera-comment.md`	The PR / MR summary comment
`theformalera-report.html`	A standalone HTML report

Run report

Schema theformalera.run/v1. A trimmed real report:

{
  "schema": "theformalera.run/v1",
  "engine": "theformalera engine 2026.10",
  "cli": "theformalera 0.9.0",
  "level": "proof",
  "runner": "local",
  "lock_digest": "sha256:7f03268e42f81adf8a710cc7d626057d9b083243a4fb27f52d818c47fe0606bf",
  "started": "2026-11-01T07:28:07+00:00",
  "seconds": 1.429,
  "summary": { "passed": 5, "failed": 1, "unknown": 0, "bounded": 0, "waived": 0 },
  "lemmas": {
    "hits": 14,
    "by_library": { "builtin": 10, "public": 0, "org": 4, "local": 0 },
    "saved_s": 2.3,
    "new": 0,
    "new_by_destination": {},
    "open_goals": 0,
    "enabled": true,
    "contribute": "org",
    "retrieved": 1,
    "org": "acme"
  },
  "coverage": {
    "Qwen/Qwen3.8-27B@1.0": {
      "covered": 6, "total": 21,
      "uncovered": ["gdn.in_proj", "gdn.conv", "gdn.core", "…"],
      "partial": [],
      "trusted": ["embed", "lm_head"]
    }
  },
  "scope": null,
  "results": [ … ]
}

Field	Meaning
`summary`	Counts per verdict. `bounded` counts PASS · BOUNDED; `waived` counts waived results, which are also counted under their verdict.
`lemmas`	The Lemma Hub line in numbers: hits per library, estimated seconds saved, new lemmas and their destinations, open goals, the contribution policy and the deposit status
`coverage`	L2 coverage per locked model
`scope`	`null` for a whole-project run; otherwise the paths or `changed: …` files it was limited to
`results`	One result record per (kernel, Spec Key)

Result record

Schema theformalera.result/v1. The record for a failure, as theformalera explain F-0001 --json prints it:

{
  "schema": "theformalera.result/v1",
  "id": "F-0001",
  "verdict": "FAILED",
  "kind": "counterexample",
  "kernel": { "name": "paged_decode_attention", "file": "kernels/attn_decode.py", "line": 28, "lang": "triton" },
  "spec": {
    "key": "Qwen/Qwen3.8-27B@1.0:layers[*].attn.core",
    "node": "layers[*].attn.core",
    "digest": "sha256:313a42af237f0db7ec729fd0d5d9230d932d829da0cbda0c43bdb4d310aaddf4"
  },
  "configs_total": 1,
  "configs_passing": 0,
  "configs_failing": 1,
  "seconds": 0.0,
  "cached": true,
  "assumptions": [],
  "warnings": [],
  "witnesses": [ { "B": 1, "seq_len": 1 }, { "B": 1, "seq_len": 17 } ],
  "witness_detail": [
    { "shape": { "B": 1, "seq_len": 1 }, "element": [0, 0, 0], "got": NaN, "expected": -0.25395343624908856,
      "detail": "o[0, 0, 0]: kernel nan, spec -0.253953", "case": { … } }
  ],
  "holds_when": "seq_len % 16 == 0",
  "suspect": { "file": "kernels/attn_decode.py", "line": 39, "expr": "seq_len // PAGE_SIZE",
               "expected": "tl.cdiv(seq_len, PAGE_SIZE)" },
  "detail": "o[0, 0, 0]: kernel -0.163625, spec -0.17983 (typical); minimal: o[0, 0, 0]: kernel nan, spec -0.253953",
  "repro": "theformalera repro F-0001",
  "configs": [ { "config": { "D": 256, "G": 6, "PAGE": 16 }, "verdict": "FAILED", "kind": "COUNTEREXAMPLE", … } ]
}

A PASS carries the proof path and its Lemma Hub fields:

{
  "schema": "theformalera.result/v1",
  "verdict": "PASS",
  "kind": "proved",
  "kernel": { "name": "silu_mul_tanh_kernel", "file": "kernels/act_fast.py", "line": 18, "lang": "triton" },
  "spec": { "key": "Qwen/Qwen3.8-27B@1.0:layers[*].mlp.act", "node": "layers[*].mlp.act",
            "digest": "sha256:313a42af237f0db7ec729fd0d5d9230d932d829da0cbda0c43bdb4d310aaddf4" },
  "proof": "proofs/silu_mul_tanh_kernel__layers____mlp_act__1df901ae78.lean",
  "lemmas": {
    "snapshot": "2026-11-01T03:49Z",
    "hits": { "builtin": 4, "public": 0, "org": 4, "local": 0 },
    "saved_estimate_s": 2.3,
    "new": [],
    "open_goals": 0
  }
}

Field	Present	Meaning
`id`	FAILED	Stable failure id
`verdict`, `kind`	always	`PASS`/`FAILED`/`UNKNOWN`, and the lower-case subtype
`witnesses`, `witness_detail`	FAILED	Shapes of the minimal and typical witnesses; the element, the kernel’s value, the spec’s value, and the `case` that rebuilds the input
`holds_when`	FAILED, when known	Where the kernel is still correct
`suspect`	FAILED, when known	Source location, expression and expected expression
`stuck_at`	UNKNOWN	The IR location the proof generator could not handle
`proof`	PASS	Path of the Lean 4 certificate, relative to `.theformalera/`
`waiver`	waived	The waiver that applied
`configs`	always	One entry per constexpr configuration, with its own verdict, kind, IR digest, certificate, axioms, hypotheses and Lemma Hub statistics

SARIF

One SARIF result per non-passing (kernel, Spec Key), plus notes for BOUNDED results:

Rule	Kind	Level
`TFE001`	counterexample	error
`TFE002`	unsafe	error
`TFE003`	overflow	error
`TFE004`	vacuous	error
`TFE005`	timeout	warning
`TFE006`	unsupported	warning
`TFE007`	bounded	warning

{
  "ruleId": "TFE001",
  "level": "error",
  "message": { "text": "paged_decode_attention -> Qwen/Qwen3.8-27B@1.0:layers[*].attn.core: FAILED (counterexample). o[0, 0, 0]: kernel -0.163625, spec -0.17983 (typical); minimal: o[0, 0, 0]: kernel nan, spec -0.253953 Correct only when seq_len % 16 == 0. Expected: tl.cdiv(seq_len, PAGE_SIZE). Run `theformalera explain F-0001`." },
  "locations": [ { "physicalLocation": { "artifactLocation": { "uri": "kernels/attn_decode.py" },
                                         "region": { "startLine": 39 } } } ],
  "partialFingerprints": { "theformalera/v1": "paged_decode_attention|Qwen/Qwen3.8-27B@1.0:layers[*].attn.core|counterexample" }
}

The location is the suspect line when there is one, else the kernel’s line. The fingerprint keeps the same alert open across runs.

PR comment

theformalera-comment.md starts with ### theformalera verify: <failed> failed, <unknown> unknown, <passed> passed. It continues with a table of kernels, the model coverage and the Lemma Hub line, and ends with a footer naming the CLI, engine, level and runner. See Continuous integration for an example.

CLI

Configuration

Formats

Run report

Result record

SARIF

PR comment

​Run report

​Result record

​SARIF

​PR comment

Run report

Result record

SARIF

PR comment