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

# Op Specs and Model Specs

> What a Lean 4 spec says, what it leaves out, and how a model's compute graph is built from it.

A spec says **what** to compute, never **how**: no memory layout, no tiling, no parallelism, no numerical tricks. Specs are written in Lean 4 over Mathlib's real numbers `ℝ`.

## Op Specs

An **Op Spec** is the definition of one operator, with parameters. Here is RMSNorm in two variants, from `specs/TheFormalEra/Ops/Norm.lean`:

```lean theme={"system"}
/-- RMSNorm with the weight applied as `w` (Qwen3, Granite, Gemma 4). -/
noncomputable def rmsnorm (eps : ℝ) (x : ι → Fin H → ℝ) (w : Fin H → ℝ) : ι → Fin H → ℝ :=
  fun t h => x t h / Real.sqrt ((∑ j, x t j ^ 2) / (H : ℝ) + eps) * w h

/-- RMSNorm in the Qwen3.5 family: the weight is applied as (1 + w) -/
noncomputable def rmsnormOffset (eps : ℝ) (x : ι → Fin H → ℝ) (w : Fin H → ℝ) : ι → Fin H → ℝ :=
  fun t h => x t h / Real.sqrt ((∑ j, x t j ^ 2) / (H : ℝ) + eps) * (1 + w h)
```

Attention is defined as softmax over the visible positions only, with grouped-query heads:

```lean theme={"system"}
/-- Softmax over the reals, normalized only over visible positions -/
noncomputable def softmax {L : ℕ} (s : Fin L → ℝ) (visible : Fin L → Prop)
    [DecidablePred visible] : Fin L → ℝ :=
  fun l => if visible l then
    Real.exp (s l) / ∑ m ∈ Finset.univ.filter visible, Real.exp (s m) else 0

/-- Causal GQA: each KV head serves G query heads; pos s is the position of query s -/
noncomputable def causalGQA {S L Hkv G D : ℕ} (scale : ℝ) (pos : Fin S → ℕ)
    (q : Fin S → Fin Hkv → Fin G → Fin D → ℝ)
    (k v : Fin L → Fin Hkv → Fin D → ℝ) : Fin S → Fin Hkv → Fin G → Fin D → ℝ :=
  fun s c g d =>
    let logit : Fin L → ℝ := fun l => scale * ∑ e, q s c g e * k l c e
    ∑ l, softmax logit (fun l => l.val ≤ pos s) l * v l c d
```

Subtracting the running max, online softmax and split-KV reduction are implementation choices. The spec does not mention them; a kernel that uses them must be proved equal to this definition. The library's theorems include `softmax_shift` (subtracting any reference value leaves softmax unchanged) and `flashAttn_eq` (online softmax with block skipping equals the attention head).

The full list of operators is on [Op Specs](https://docs.theformalera.com/models/op-specs.md).

## Model Specs

A **Model Spec** fixes every configuration constant of one checkpoint and assembles Op Specs into a compute graph. The constants are transcribed from the checkpoint's published `config.json`; for example, Qwen3.8-27B in `specs/TheFormalEra/Spec/Registry.lean`:

```lean theme={"system"}
def qwen3_8_27b : Qwen35Hyper where
  vocab_size := 248320
  hidden_size := 5120
  intermediate_size := 17408
  layer_types := cycle 16 [.linear, .linear, .linear, .full]
  num_attention_heads := 24
  num_key_value_heads := 4
  head_dim := 256
  partial_rotary_factor := 1 / 4
  rope_theta := 10000000
  rms_norm_eps := 1e-6
  linear_num_key_heads := 16
  linear_num_value_heads := 48
  linear_key_head_dim := 128
  linear_value_head_dim := 128
  linear_conv_kernel_dim := 4
  tie_word_embeddings := false
```

Each named sub-computation of a layer is a **node**: `input_norm`, `attn.qkv_proj`, `attn.core`, `mlp.act`, and so on. A node references an Op Spec and supplies its parameters (`H = 5120`, `eps = 1e-6`). The graph also records the value flow: which node's output feeds which node's input in every layer.

```text theme={"system"}
$ theformalera spec show 'Qwen/Qwen3.8-27B@1.0:layers[*].mlp.act'
mlp.act   TheFormalEra.Ops.siluMul  ·  64 layer(s)
├── y[t,i] = silu(gate_up[t,i]) · gate_up[t,17408+i]
├── constants: I=17408, act=silu
├── tensors
│   ├── gate_up  in      [T, 34816]  bf16
│   └── y        out     [T, 17408]  bf16
└── shape domain: T ∈ [1, 262144]
```

With `--lean`, the command also prints the Op Spec's Lean definition:

```lean theme={"system"}
noncomputable def siluMul {I : ℕ} (gu : ι → Fin (2 * I) → ℝ) : ι → Fin I → ℝ :=
  fun t i => silu (gu t ⟨i.val, by omega⟩) * gu t ⟨I + i.val, by omega⟩
```

## Shape and value domains

Disposable inference systems are built for one model, so its dimensions are constants. Only runtime dimensions are symbolic. Each Model Spec has a default **shape domain**:

| Symbol | Meaning | Qwen3.8-27B default |
| - | - | - |
| `T` | Tokens in a batch (prefill) | `[1, 262144]` |
| `B` | Sequences in a decode batch | `[1, 256]` |
| `S` | Cached sequence length | `[1, 262144]` |
| `page_size` | KV-cache page size | `16` |

and a **value domain** used only for the overflow check: inputs are `bf16` activations with `|x| ≤ 65504`, and weights with `|w| ≤ 64`.

A proof holds for every point in the domain. An annotation may **narrow** the domain (`domain={"T": (1, 8192)}`), never widen it: widening is an error.

## Why Lean 4

* The spec, the lifted kernel semantics and the equivalence proof live in one system. The theorem says "kernel semantics = spec" with no translation step in between.
* The Lean 4 kernel checks every proof, so a closed-source engine does not reduce what you can trust.
* Mathlib supplies the real numbers, sums, matrices and `Real.exp`, with a large library of proved facts.
* You never need to write Lean. `theformalera spec show` and the Spec Hub site render the formulas.

## The oracle

The spec library also builds an executable, `theformalera-spec`, that evaluates any Model Spec on concrete weights and tokens. Its evaluators are proved equal to the spec (`runTrace_fst`, and the `@[csimp]` theorems `linear_eq_linearPar`, `seqMap_eq_seqMapPar`). This is what [model conformance](https://docs.theformalera.com/conformance/overview.md) compares PyTorch implementations against.


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