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

# Write and check a spec

> Draft a Model Spec from a torch.export graph, add a model to the Lean library, and check it.

Most users never write a spec: the Model Specs on Spec Hub are written by us or by model vendors. Read this page if you need a spec for a model that is not on the Hub yet, or a private spec for an unreleased model.

## Draft from a reference implementation

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

`spec new` reads a graph exported with `torch.export`. It strips engineering nodes (KV-cache updates, device and dtype moves, views that only reorganise memory, backend branches) and maps recognised subgraphs onto Op Specs:

| ATen pattern | Op Spec |
| - | - |
| `pow(x, 2) → mean(-1) → add(eps) → rsqrt → mul(x) → mul(w)` | `rmsnorm` / `rmsnormOffset` |
| `linear(x, W)`, `mm`, `matmul` with a weight parameter | `linear` |
| `silu(a) * b` | `siluMul` |
| `scaled_dot_product_attention`, softmax(QKᵀ)·V | `causalGQA` |
| `cos`/`sin` tables, `cat(-x2, x1)` rotate-half | `rope` |
| `embedding` | `embed` |

Unrecognised compute nodes are kept as placeholders marked `-- REVIEW:`. The draft is a starting point: publish it only after a human review and a [conformance check](https://docs.theformalera.com/conformance/overview.md).

## How models are defined in the library

The spec library (`specs/`) defines each architecture **family** as a function from its Hugging Face hyperparameters to a model configuration (`ModelCfg`). That is where the architecture knowledge lives: which norms, which RoPE variant, which multipliers. `specs/TheFormalEra/Spec/Families.lean` has five families today: `Qwen3Hyper`, `Qwen35Hyper`, `GraniteHyper`, `Gemma4Hyper` and `MuseHyper`.

A model is then one record of hyperparameters plus one registry entry (`specs/TheFormalEra/Spec/Registry.lean`):

```lean theme={"system"}
def qwen3_0_6b : Qwen3Hyper where
  vocab_size := 151936
  hidden_size := 1024
  intermediate_size := 3072
  num_hidden_layers := 28
  num_attention_heads := 16
  num_key_value_heads := 8
  head_dim := 128
  rms_norm_eps := 1e-6
  rope_theta := 1000000
  tie_word_embeddings := true
  sliding_window := none
  max_window_layers := 28

def qwen3_0_6b_reduced : Qwen3Hyper :=
  { qwen3_0_6b with vocab_size := 512, hidden_size := 64, intermediate_size := 192,
                    num_hidden_layers := 4, num_attention_heads := 16, num_key_value_heads := 8,
                    head_dim := 8, max_window_layers := 4 }

def registry : List ModelEntry := [
  ⟨"Qwen/Qwen3-0.6B", .qwen3 qwen3_0_6b, .qwen3 qwen3_0_6b_reduced, "Qwen3ForCausalLM"⟩,
  …]
```

Every family also has `toHF`, which renders the hyperparameters back in `config.json` form. The conformance check compares that rendering with the published `config.json`, field by field.

To add a checkpoint of an existing family, add its record, a reduced record with the same layer pattern, and a registry entry. To add a new architecture, add a family. The compute graph (`TheFormalEra.Models.Graph`), the executable oracle and the CLI then pick it up.

> [!TIP]
>
> The reduced configuration must have the **same architecture**: the same layer-type pattern, attention variants, norms and multipliers, at a small width. The theorem `reduced_same_architecture` checks this for every registry entry.

## Check a spec package

```bash theme={"system"}
theformalera spec check specs/
```

`spec check`:

1. runs `lake build`: the definitions type-check and every proof is checked;
2. runs the axiom audit (`Audit.lean`): every listed theorem depends only on `propext`, `Classical.choice` and `Quot.sound`;
3. exports each model's graph and checks it is connected: every node input is produced by another node, except the graph's inputs (`tokens`, `positions`, `seq_lens`) and cache values.

## Check it against the reference implementation

```bash theme={"system"}
theformalera-conformance verify <org>/<model>
```

This runs the official Hugging Face implementation against your spec, layer by layer, in float64. See [Model conformance](https://docs.theformalera.com/conformance/overview.md). The spec and the reference must agree before the spec is published.

## Publish

```bash theme={"system"}
theformalera-hub publish --specs specs --store <store> --version 1.1.0 --key publisher.pem \
    --model <org>/<model> --conformance conformance-report.json
```

See [Publish specs](https://docs.theformalera.com/self-hosting/publish-specs.md). Published versions are immutable: publishing an existing version with a different digest is refused. Bump the version instead.


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