Supported models

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)

$ 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)