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

# Supported models

> The Lean 4 Model Specs on Spec Hub, their architectures and their conformance status.

Spec Hub has a Lean 4 Model Spec for each of these checkpoints. Every spec is conformance-checked against the official Hugging Face implementation; see [Results](https://docs.theformalera.com/conformance/results.md).

| Model key | Layers | Parameters | Architecture | Conformance |
| - | -: | -: | - | - |
| [`Qwen/Qwen3-0.6B`](https://docs.theformalera.com/models/qwen3-0-6b) | 28 | 0.60 B | Dense GQA attention, q/k norms | ✓ 1.5e-15 · checkpoint ✓ |
| [`Qwen/Qwen3.8-27B`](https://docs.theformalera.com/models/qwen3-8-27b) | 64 | 26.90 B | 48 Gated DeltaNet + 16 gated attention, `(1 + w)` norms | ✓ 4.1e-14 |
| [`google/gemma-4-12B`](https://docs.theformalera.com/models/gemma-4-12b) | 48 | 11.91 B | 40 sliding + 8 global, sandwich norms, soft-cap 30 | ✓ 6.7e-16 |
| [`google/gemma-4-31B`](https://docs.theformalera.com/models/gemma-4-31b) | 60 | 30.70 B | 50 sliding + 10 global, sandwich norms, soft-cap 30 | ✓ 8.6e-16 |
| [`ibm-granite/granite-4.2-3b`](https://docs.theformalera.com/models/granite-4-2-3b) | 40 | 3.66 B | Dense GQA attention, attention scale 1/64 | ✓ 2.3e-15 · checkpoint ✓ |
| [`ibm-granite/granite-4.2-8b`](https://docs.theformalera.com/models/granite-4-2-8b) | 40 | 8.79 B | Dense GQA attention, attention scale 1/128 | ✓ 1.6e-15 |
| [`ibm-granite/granite-4.2-30b`](https://docs.theformalera.com/models/granite-4-2-30b) | 64 | 29.28 B | Dense GQA attention, attention scale 1/128 | ✓ 1.7e-15 |
| [`meta-models/Muse-Glimmer-30B`](https://docs.theformalera.com/models/muse-glimmer-30b) | 52 | 27.85 B | 39 sliding + 13 NoPE global, gated attention, soft-cap 20 | ✓ 7.7e-15 |

"✓ 1.5e-15" is the maximum relative error between the official implementation and the spec, layer by layer, in float64. "checkpoint ✓" means the weight-level cross-check on the published checkpoint has been run too.

## Browse a spec

```bash theme={"system"}
theformalera-conformance models                          # this table, from the Lean spec
theformalera-conformance spec Qwen/Qwen3.8-27B           # the architecture tree
theformalera spec show 'Qwen/Qwen3.8-27B@1.0:layers[*].attn.core'   # one node (in a project that locks it)
```

```text theme={"system"}
$ theformalera-conformance spec Qwen/Qwen3.8-27B
Qwen/Qwen3.8-27B  ·  qwen3_5  ·  26,895,998,464 parameters
├── embedding
│   └── vocab 248320 → hidden 5120,  × 1
├── 64 decoder layers  (norm (1+w)·x̂, ε=1e-06)
│   ├── Gated DeltaNet  the other 48 layers
│   │   ├── 16 key heads × 128, 48 value heads × 128, causal conv width 4
│   │   └── S' = e^γ·S;  S = S' + β·k̂ ⊗ (v − S'ᵀk̂);  o = Sᵀq̂;  gated RMSNorm
│   ├── attention (full causal)  layers 3, 7, …, 63
│   │   ├── 24 query heads / 4 kv heads, head dim 256, scale 1/√256
│   │   ├── q/k RMSNorm (1+w)·x̂, sigmoid output gate (fromQuery)
│   │   └── RoPE: θ=10000000 rot=64 denom=64 active=32
│   └── MLP: down(act(gate·x) ⊙ up·x), act = silu, width 17408
└── head
    └── final norm (1+w)·x̂, lm_head separate
well formed: True (checked by `decide` in TheFormalEra.Proofs.Registry)
```

## What every spec covers

* **The text path.** Vision and audio towers and multi-token-prediction heads are out of scope. For text-only input, Qwen3.8's mRoPE sections coincide, so the spec defines ordinary partial RoPE.
* **Decode attention** (`attn.core`) is specified for one new query per sequence over `seq_lens[b]` cached positions. That is what decode kernels compute.
* **Dense models only.** Mixture-of-experts models are not supported yet.

## Facts proved about the specs

The spec library proves these properties in Lean, and the Lean kernel checks them with standard axioms only:

| Theorem | Statement |
| - | - |
| `forward_causal` | Every model of the specification is causal (all configurations, all scalar types) |
| `attnHead_local` | An attention head only reads visible positions (causal mask + sliding window) |
| `softmax_shift` | Softmax is invariant under the subtracted reference value |
| `attnWeights_distribution` | Attention weights form a probability distribution over the visible keys |
| `rope_relative` | RoPE encodes relative positions: ⟨R\_p q, R\_p' k⟩ = ⟨R\_(p−p') q, k⟩ |
| `rope_isometry` | RoPE preserves inner products |
| `deltaRule_causal` | The gated delta rule is causal |
| `deltaStep_read_key` | The delta rule stores `v` under a unit key `k` exactly (β = 1, no decay) |
| `causalConv_causal` | The Gated DeltaNet's depthwise convolution is causal |
| `registry_wellFormed` | All 8 checkpoint specs and their reduced versions are well formed |
| `reduced_same_architecture` | Each reduced configuration has the architecture of its checkpoint |
| `qwen3_8_27b_pattern` | Qwen3.8-27B: layer `i` is full attention iff `i % 4 = 3` |
| `gemma4_12b_pattern`, `gemma4_31b_pattern` | Gemma 4: layer `i` is global iff `i % 6 = 5` |
| `museGlimmer_global_iff_nope` | Muse Glimmer: the global layers are exactly the NoPE layers |
| `qwen3_0_6b_params` | The Qwen3-0.6B text model has 596,049,920 parameters |
| `flashAttn_eq` | FlashAttention (online softmax, block skipping) equals the spec's attention head |
| `chunkDeltaRule_eq` | The chunked (WY-form) gated delta rule equals the recurrence, for every chunk size |
| `rmsNormTiled_eq` | Tiled RMSNorm equals the spec's RMSNorm, for every block size and weight kind |

The full list of 37 audited theorems is in `specs/Audit.lean`. Run `theformalera-conformance prove` to rebuild and re-audit them.


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