CLI overview

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

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

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.

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