Verification commands

verify

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.

Option	Default	Meaning
`PATHS`	`[scan] include`	Files or directories to verify
`--level`	`[verify] level`	`proof`, `bounded` or `quick`; see Verdicts
`--runner`	`[verify] runner`	Where the engine runs; see Run modes
`--format`	`table`	`json` prints the 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

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.

repro

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:

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

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.

mcp

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.

CLI

Configuration

Formats

verify

explain

repro

guards

mcp

​verify

​explain

​repro

​guards

​mcp

verify

explain

repro

guards

mcp