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

# Reports

> The run report, the result record, SARIF, the PR comment and the HTML report.

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.

```bash theme={"system"}
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:

```json theme={"system"}
{
  "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:

```json theme={"system"}
{
  "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:

```json theme={"system"}
{
  "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 |

```json theme={"system"}
{
  "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](https://docs.theformalera.com/guides/ci.md#the-pull-request-comment) for an example.


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