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

# Project commands

> login, init, scan, pull, annotate and version.

## login

```bash theme={"system"}
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

```bash theme={"system"}
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

```bash theme={"system"}
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.

```text theme={"system"}
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

```bash theme={"system"}
theformalera pull [--update] [--no-build]
```

For every model under `[models]`:

1. resolve the version: the locked one if it still satisfies the requirement, else the newest that does;
2. download the package and check its content hash against the lock (a mismatch stops the command);
3. verify the publisher's signature;
4. install it into the content-addressed cache (`~/.cache/theformalera/specs/<digest>`);
5. 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"`) |

```text theme={"system"}
✓ Qwen/Qwen3.8-27B@1.0.0  sha256:313a42af237f…  signed theformalera (verified)
wrote theformalera.lock (1 spec)
```

## annotate

```bash theme={"system"}
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

```bash theme={"system"}
theformalera version
```

```text theme={"system"}
theformalera 0.9.0 · theformalera engine 2026.10
```


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