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

# Verification commands

> verify, explain, repro, guards and mcp.

## verify

```bash theme={"system"}
theformalera verify [PATHS]... [--level proof|bounded|quick] [--runner local|cloud|on-prem]
                    [--format table|json] [--changed-only REF] [--report-dir DIR] [--sarif FILE] [--no-lemmas]
```

Verify annotated kernels against their specs and apply the [policy](https://docs.theformalera.com/guides/policy-and-waivers.md).

| Option | Default | Meaning |
| - | - | - |
| `PATHS` | `[scan] include` | Files or directories to verify |
| `--level` | `[verify] level` | `proof`, `bounded` or `quick`; see [Verdicts](https://docs.theformalera.com/concepts/verdicts.md#levels) |
| `--runner` | `[verify] runner` | Where the engine runs; see [Run modes](https://docs.theformalera.com/guides/run-modes.md) |
| `--format` | `table` | `json` prints the [run report](https://docs.theformalera.com/reference/reports.md#run-report) to stdout |
| `--changed-only REF` | — | Only kernels in files changed since `REF` (`git diff --name-only REF...HEAD`) |
| `--report-dir DIR` | — | Write `theformalera-report.json`, `theformalera.sarif`, `theformalera-comment.md` and `theformalera-report.html` |
| `--sarif FILE` | — | Write a SARIF file |
| `--no-lemmas` | off | Disable the Lemma Hub: no retrieval, no built-in lemmas in the search, no deposit (a baseline) |

On a terminal, a live line shows the current kernel and stage (`lifting`, `searching for counterexamples`, `proving (Lean 4 · Lemma Hub)`). The run ends with the results table, the summary, and the Lemma Hub line. With `--format table`, policy problems such as expired waivers are printed after the table.

A run over a subset of the project (`PATHS` or `--changed-only`) is recorded as partial; `signoff` refuses partial runs.

## explain

```bash theme={"system"}
theformalera explain FAILURE_ID [--json]
```

Show a failure of the last run: the failing configs, the minimal and typical witnesses, `correct only when`, details, notes and the suspect line. `--json` prints the full [result record](https://docs.theformalera.com/reference/reports.md#result-record).

## repro

```bash theme={"system"}
theformalera repro FAILURE_ID [-o repro.py] [--witness typical|minimal]
```

Write a standalone PyTorch script that runs the kernel on the GPU with the counterexample input, and compares it with the spec's float64 reference interpreter:

```python theme={"system"}
case = tfe.load_case("F-0001", witness="typical")
paged_decode_attention[case.grid](**case.kernel_args, D=256, G=6, PAGE=16)
out = case.output("o")
ref = tfe.spec_eval(case.spec_key, **{k: case.spec_args[k] for k in ['q', 'k', 'v', 'seq_lens']})
print("max abs diff:", (out.double() - ref).abs().max().item())
```

Run it from the project root. It needs a GPU, Triton and PyTorch. Failures without a concrete input, such as an integer-overflow witness found by SMT, cannot be reproduced this way, and `repro` says so.

## guards

```bash theme={"system"}
theformalera guards [--emit kernels/_theformalera_guards.py]
```

Generate a Python module with one `guard_<kernel>(...)` function per annotated kernel. It checks every `assume=` entry and every scalar bound to a model constant. See [Layouts and assumptions](https://docs.theformalera.com/guides/layouts-and-assumptions.md#runtime-guards).

## mcp

```bash theme={"system"}
theformalera mcp [--transport stdio|streamable-http]
```

Start the MCP server for coding agents, with the tools `spec.get`, `spec.nodes`, `verify.quick`, `verify.full`, `verify.job`, `explain` and `lemma.search`. It needs the `mcp` extra. See [Coding agents](https://docs.theformalera.com/guides/coding-agents.md).


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