Project commands

theformalera login [--token TOKEN] [--hub URL]

Store a Spec Hub API token. Without --token, the command opens <hub>/login?cli=1 in the browser and prompts for the token shown after sign-in.

Option	Default	Meaning
`--token`	prompt	The API token
`--hub`	the project’s `hub`, else `https://hub.theformalera.com`	The Hub to log in to

The token is written to ~/.config/theformalera/credentials.json (mode 0600), keyed by Hub URL. THEFORMALERA_TOKEN takes precedence over the stored token, so CI never needs login.

init

theformalera init [--name NAME] [--model KEY]... [--runner local|cloud|on-prem] [--force]

Detect Triton (@triton.jit) and CUDA/CUTLASS (__global__, cutlass) code and write theformalera.toml. init also:

writes AGENTS.md (verification rules for coding agents), unless one exists;
adds .theformalera/ to .gitignore, if there is one;
finds a CUTLASS include directory (third_party/cutlass/include or cutlass/include);
sets [lemmas] contribute to the default for the run mode and plan (off for local).

Option	Default	Meaning
`--name`	the directory name	`[project] name`
`--model`	none	A model key to add under `[models]` with `version = "^1.0"`; repeatable
`--runner`	`local`	`[verify] runner`, which also sets the Lemma Hub default
`--force`	off	Overwrite an existing `theformalera.toml`

scan

theformalera scan [PATHS]... [--json]

List every annotated kernel, and the coverage of each locked model’s compute graph. scan reads annotations from the source and never imports your modules.

Found 5 annotated kernels (5 Triton)
  kernels/act.py:13          silu_mul_kernel         -> layers[*].mlp.act
  kernels/act_fast.py:18     silu_mul_tanh_kernel    -> layers[*].mlp.act   (autotune: 4 configs)
  kernels/attn_decode.py:28  paged_decode_attention  -> layers[*].attn.core
  kernels/norm.py:14         rmsnorm_kernel          -> layers[*].input_norm, layers[*].post_attn_norm
  kernels/residual.py:13     residual_add_kernel     -> layers[*].attn_residual
Coverage Qwen/Qwen3.8-27B@1.0: 5 of 21 graph nodes
  not covered: embed, gdn.in_proj, gdn.conv, …

Kernels under [policy] require_annotation without an annotation are listed at the end. --json prints one object per kernel: name, file, line, language, kind (kernel or launcher), keys, parameters, grid, bind, layout, domain, assume, configs and autotune configs.

pull

theformalera pull [--update] [--no-build]

For every model under [models]:

resolve the version: the locked one if it still satisfies the requirement, else the newest that does;
download the package and check its content hash against the lock (a mismatch stops the command);
verify the publisher’s signature;
install it into the content-addressed cache (~/.cache/theformalera/specs/<digest>);
unless --no-build, build its Lean workspace (reusing $THEFORMALERA_MATHLIB if set, else lake exe cache get).

Then report spec security advisories for the locked versions, and write theformalera.lock.

Option	Meaning
`--update`	Re-resolve versions instead of keeping the locked ones
`--no-build`	Skip the Lean build (for `runner = "cloud"`)

✓ Qwen/Qwen3.8-27B@1.0.0  sha256:313a42af237f…  signed theformalera (verified)
wrote theformalera.lock (1 spec)

annotate

theformalera annotate PATH [--model KEY]

Draft @tfe.implements annotations for the unannotated @triton.jit kernels in a file, from parameter names and data flow. Drafts are printed, never written. A wrong draft can only make verification fail, never pass.

Option	Default	Meaning
`--model`	the only locked model	Which locked model to match nodes against

version

theformalera version

theformalera 0.9.0 · theformalera engine 2026.10

CLI

Configuration

Formats

init

scan

pull

annotate

version

​login

​init

​scan

​pull

​annotate

​version

login

init

scan

pull

annotate

version