Qwen3-0.6B - The Formal Era

conformance ✓ spec 1.0 qwen3 The Model Spec of Qwen/Qwen3-0.6B in TheFormalEra.Spec.Registry. The constants below are transcribed from its published config.json, and the official transformers.Qwen3ForCausalLM is checked against them.

At a glance


Model key	`Qwen/Qwen3-0.6B`
Parameters (text model)	596,049,920
Layers	28 (28 full attention)
Hidden size	1,024
MLP width	3,072 (silu)
Vocabulary	151,936
Norm	`w·x̂`, ε = 1e-06
Embedding	tied to the LM head
Logits	no soft-capping
Hugging Face class	`Qwen3ForCausalLM`
Shape domain	`T` ∈ [1, 40,960] tokens, `B` ∈ [1, 256] sequences, `S` ∈ [1, 40,960] cached positions, page size 16

What to watch for

Every layer is full causal attention: 16 query heads share 8 KV heads (2 query heads per KV head), head dim 128, scale 1/√128.
Queries and keys get a per-head RMSNorm (attn.qk_norm) before RoPE.
RMSNorm weights are applied as w (rmsnorm).
The language-model head is tied to the embedding.

Compute-graph nodes

Use these paths in Spec Keys: Qwen/Qwen3-0.6B@1.0:layers[*].<node> for per-layer nodes, Qwen/Qwen3-0.6B@1.0:<node> for the others.

Node	Op Spec	Layers	Formula	Constants
`embed`	`embed`	—	`y[t] = 1 · w[tokens[t]]`	mul=1, norm=False
`input_norm`	`rmsnorm`	all 28	`y[t,i] = x[t,i] / √(Σⱼ x[t,j]² / H + ε) · w[i]`	H=1024, eps=1e-06
`attn.qkv_proj`	`linear`	all 28	`y[t,n] = Σₖ x[t,k] · w[n,k]`	K=1024, N=4096
`attn.qk_norm`	`rmsnorm`	all 28	`per head: y[t,i] = x[t,i] / √(Σⱼ x[t,j]² / H + ε) · w[i]`	D=128, eps=1e-06
`attn.rope`	`rope`	all 28	`rotate pairs (i, i + 64) by pos · θ^(-2i/128), i < 64; coordinates ≥ 128 unchanged`	D=128, active=64, denom=128, rot=128, theta=1000000
`attn.core`	`decodeGQA`	all 28	`o[b,h] = Σ_{s < seq_lens[b]} softmax_s(1/√128 · ⟨q[b,h], k[b,s,h / 2]⟩) · v[b,s,h / 2]`	D=128, heads=16, kv_heads=8, scale=1/√128
`attn.o_proj`	`linear`	all 28	`y[t,n] = Σₖ x[t,k] · w[n,k]`	K=2048, N=1024
`attn_residual`	`residual`	all 28	`y = x + h`	H=1024, layer_scalar=False, r=1
`post_attn_norm`	`rmsnorm`	all 28	`y[t,i] = x[t,i] / √(Σⱼ x[t,j]² / H + ε) · w[i]`	H=1024, eps=1e-06
`mlp.gate_up`	`linear`	all 28	`y[t,n] = Σₖ x[t,k] · w[n,k]`	K=1024, N=6144
`mlp.act`	`siluMul`	all 28	`y[t,i] = silu(gate_up[t,i]) · gate_up[t,3072+i]`	I=3072, act=silu
`mlp.down`	`linear`	all 28	`y[t,n] = Σₖ x[t,k] · w[n,k]`	K=3072, N=1024
`mlp_residual`	`residual`	all 28	`y = x + h`	H=1024, layer_scalar=False, r=1
`final_norm`	`rmsnorm`	—	`y[t,i] = x[t,i] / √(Σⱼ x[t,j]² / H + ε) · w[i]`	H=1024, eps=1e-06
`lm_head`	`lmHead`	—	`z = x wᵀ`	mul=1, tied=True

Nodes listed twice have different constants in different layers (for example, sliding-window and global attention). A kernel annotated with layers[*].<node> is verified against each variant.

Tensors of the main nodes

Node	Inputs and outputs
`embed`	`tokens` [T], `y` [T, 1024]
`input_norm`	`x` [T, 1024], `y` [T, 1024]
`attn.qkv_proj`	`x` [T, 1024], `y` [T, 4096]
`attn.qk_norm`	`q` [T, 16, 128], `k` [T, 8, 128], `q_out` [T, 16, 128], `k_out` [T, 8, 128]
`attn.rope`	`q` [T, 16, 128], `k` [T, 8, 128], `pos` [T], `q_out` [T, 16, 128], `k_out` [T, 8, 128]
`attn.core`	`q` [B, 16, 128], `k` [B, S, 8, 128], `v` [B, S, 8, 128], `seq_lens` [B], `o` [B, 16, 128]
`attn.o_proj`	`x` [T, 2048], `y` [T, 1024]
`attn_residual`	`x` [T, 1024], `h` [T, 1024], `y` [T, 1024]
`post_attn_norm`	`x` [T, 1024], `y` [T, 1024]
`mlp.gate_up`	`x` [T, 1024], `y` [T, 6144]
`mlp.act`	`gate_up` [T, 6144], `y` [T, 3072]
`mlp.down`	`x` [T, 3072], `y` [T, 1024]
`mlp_residual`	`x` [T, 1024], `h` [T, 1024], `y` [T, 1024]
`final_norm`	`x` [T, 1024], `y` [T, 1024]
`lm_head`	`x` [T, 1024], `logits` [T, 151936]

Conformance

The official transformers.Qwen3ForCausalLM agrees with this spec, layer by layer in float64, to a maximum relative error of 1.5e-15 (reduced-width profile, 2 weight draws × 2 lengths). On the published checkpoint, the full-size spec evaluated by the Lean oracle agrees with the official implementation to 7.7e-15 on a real prompt (85.5 s).

theformalera-conformance verify Qwen/Qwen3-0.6B                    # the official implementation
theformalera-conformance verify Qwen/Qwen3-0.6B path/to/model.py   # your implementation
theformalera-conformance spec Qwen/Qwen3-0.6B                      # the architecture, as Lean derives it

Published configuration

The hyperparameters as the spec renders them (config.json form)

{
  "vocab_size": 151936,
  "use_sliding_window": false,
  "tie_word_embeddings": true,
  "sliding_window": null,
  "rope_parameters": {
    "rope_type": "default",
    "rope_theta": 1000000
  },
  "rms_norm_eps": 1e-06,
  "num_key_value_heads": 8,
  "num_hidden_layers": 28,
  "num_attention_heads": 16,
  "max_window_layers": 28,
  "intermediate_size": 3072,
  "hidden_size": 1024,
  "hidden_act": "silu",
  "head_dim": 128,
  "attention_bias": false,
  "architectures": [
    "Qwen3ForCausalLM"
  ]
}

⌘I