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

# CLI overview

> Every command of the three command-line tools, and their common behaviour.

The Formal Era ships three command-line tools:

| Tool | Package | For |
| - | - | - |
| `theformalera` | `theformalera` | Projects: annotate, verify, explain, sign off |
| `theformalera-conformance` | `theformalera-conformance` | Checking PyTorch model implementations against Model Specs |
| `theformalera-hub` | `theformalera-hub` | Operating a Spec Hub: publish specs, serve the API, admit lemmas |

## theformalera

```text theme={"system"}
 Usage: theformalera [OPTIONS] COMMAND [ARGS]...

 Formal verification of inference kernels against Lean 4 specs from Spec Hub.
```

| Command | Does | Page |
| - | - | - |
| `login` | Store a Spec Hub token | [Project](https://docs.theformalera.com/reference/cli/project.md#login) |
| `init` | Detect Triton / CUDA code, write `theformalera.toml` and `AGENTS.md` | [Project](https://docs.theformalera.com/reference/cli/project.md#init) |
| `scan` | List annotated kernels and graph coverage | [Project](https://docs.theformalera.com/reference/cli/project.md#scan) |
| `pull` | Resolve, download, check and lock specs; build the Lean workspace | [Project](https://docs.theformalera.com/reference/cli/project.md#pull) |
| `annotate` | Draft `@tfe.implements` annotations | [Project](https://docs.theformalera.com/reference/cli/project.md#annotate) |
| `version` | Print the CLI and engine versions | [Project](https://docs.theformalera.com/reference/cli/project.md#version) |
| `verify` | Verify kernels against their specs | [Verification](https://docs.theformalera.com/reference/cli/verification.md#verify) |
| `explain` | Show a failure's witnesses, failing region and suspect line | [Verification](https://docs.theformalera.com/reference/cli/verification.md#explain) |
| `repro` | Write a GPU reproduction script for a failure | [Verification](https://docs.theformalera.com/reference/cli/verification.md#repro) |
| `guards` | Generate runtime guards for every assumption | [Verification](https://docs.theformalera.com/reference/cli/verification.md#guards) |
| `mcp` | Start the MCP server for coding agents | [Verification](https://docs.theformalera.com/reference/cli/verification.md#mcp) |
| `coverage` | L2: graph nodes covered by passing kernels | [Release](https://docs.theformalera.com/reference/cli/release.md#coverage) |
| `trace` | Record the kernel launch sequence of a program | [Release](https://docs.theformalera.com/reference/cli/release.md#trace) |
| `signoff` | Produce a signed release certificate | [Release](https://docs.theformalera.com/reference/cli/release.md#signoff) |
| `cert verify` | Deployment gate: check a certificate | [Release](https://docs.theformalera.com/reference/cli/release.md#cert-verify) |
| `spec show` · `spec new` · `spec check` | Browse, draft and check Lean 4 specs | [Specs](https://docs.theformalera.com/reference/cli/specs.md) |
| `lemma show` · `search` · `list` · `preview` | View, search and preview lemmas | [Lemmas](https://docs.theformalera.com/reference/cli/lemmas.md) |

## Common behaviour

* **Project root.** Every project command looks for `theformalera.toml` in the current directory and its parents. Without one, it fails with `no theformalera.toml found (run \`theformalera init\`)\`.
* **State.** Results of the last run live in `.theformalera/`: `last-run.json`, `failures.json` (the stable failure ids), `proofs/`, `cache/` and `lemmas/`. Add `.theformalera/` to `.gitignore`; `init` does this.
* **Errors** go to stderr as `error: <message>`.
* **Machine-readable output.** `scan`, `explain`, `coverage` and every `lemma` command take `--json`; `verify` takes `--format json`.

## Exit status

| Command | 0 | 1 | 2 |
| - | - | - | - |
| `verify` | Policy passes | Policy fails (FAILED, UNKNOWN, BOUNDED under `require_level = "proof"`, an expired waiver, an unannotated kernel) | Usage or configuration error |
| `cert verify` | Certificate valid for the requirement | Invalid signature, too low a level, wrong commit, or proof mismatch | Usage error |
| `spec check` | Builds, audits and the graph checks | Build or audit failed | Lean not installed |
| `theformalera-conformance verify` | VERIFIED | NOT VERIFIED | Unknown model key |
| Other commands | Success | — | Error |


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