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

# Spec commands

> spec show, spec new and spec check.

## spec show

```bash theme={"system"}
theformalera spec show KEY [--lean]
```

Show a spec node from a locked spec package: its Op Spec, formula, constants, tensors, shape domain and the number of layers it appears in. `--lean` also prints the Op Spec's Lean 4 definition.

```text theme={"system"}
$ theformalera spec show 'Qwen/Qwen3.8-27B@1.0:layers[*].input_norm'
input_norm   TheFormalEra.Ops.rmsnormOffset  ·  64 layer(s)
├── y[t,i] = x[t,i] / √(Σⱼ x[t,j]² / H + ε) · (1 + w[i])
├── constants: H=5120, eps=1e-06
├── tensors
│   ├── x        in      [T, 5120]  bf16
│   ├── w        weight  [5120]  bf16
│   ├── y        out     [T, 5120]  bf16
│   └── eps      scalar  []  f32
└── shape domain: T ∈ [1, 262144]
```

The key must name a node (`<model>@<version>:<layer-path>`), and the model must be locked in the current project. To browse a model without a project, use `theformalera-conformance spec <model>` or the [Spec Hub pages](https://docs.theformalera.com/models/index.md).

## spec new

```bash theme={"system"}
theformalera spec new --from-export model.pt2 --name Acme.MyModel [-o Draft.lean]
```

Draft a Lean 4 Model Spec from a `torch.export` program. Engineering nodes (KV cache, device and dtype moves, memory-only views, backend branches) are stripped. Recognised subgraphs become Op Spec instances, and anything else is marked `-- REVIEW:`. See [Write and check a spec](https://docs.theformalera.com/guides/write-a-spec.md).

It reports how many graph nodes it read, how many Op Spec instances it produced, how many engineering nodes it stripped, and how many need review:

```text theme={"system"}
✓ wrote Draft.lean: <n> graph nodes → <m> Op Spec instances (<k> engineering nodes stripped, <r> need review)
```

## spec check

```bash theme={"system"}
theformalera spec check [PATH]
```

Check a spec package (a Lake workspace; default `.`):

1. `lake build`: types, dimensions and every proof;
2. `lake env lean Audit.lean`, if present: every audited theorem uses only `propext`, `Classical.choice` and `Quot.sound`;
3. if the `theformalera-spec` executable is built: for each model, the graph's inputs are all produced by another node, a graph input or a cache value.

```text theme={"system"}
$ theformalera spec check specs
✓ compiled: types and dimensions check
✓ 37/37 theorems kernel-checked, axioms: propext, Classical.choice, Quot.sound only
✓ Qwen/Qwen3-0.6B: graph of 339 node instances, 15 variants
✓ Qwen/Qwen3.8-27B: graph of 787 node instances, 21 variants
✓ google/gemma-4-12B: graph of 723 node instances, 24 variants
✓ google/gemma-4-31B: graph of 903 node instances, 24 variants
✓ ibm-granite/granite-4.2-3b: graph of 443 node instances, 14 variants; unconnected inputs: L0.k_normed,
L0.q_normed, L1.k_normed, L1.q_normed
…
✓ meta-models/Muse-Glimmer-30B: graph of 770 node instances, 19 variants; unconnected inputs: L11.q_rot,
L15.q_rot, L19.q_rot, L23.q_rot
```

"Unconnected inputs" is a warning, not a failure: a node reads a graph value that no other node produces. In spec 1.0 this happens where a model skips a step: Granite has no q/k norm before RoPE, and Muse Glimmer's NoPE layers have no RoPE before attention. The value flow then names the skipped step's output. It does not affect what each node computes; it does affect L3 data-flow matching across those nodes.


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