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

# granite-4.2-3b

> Dense Granite: GQA attention with a µP-style attention multiplier, SwiGLU.

conformance ✓spec 1.0granite

The Model Spec of [`ibm-granite/granite-4.2-3b`](https://huggingface.co/ibm-granite/granite-4.2-3b) in `TheFormalEra.Spec.Registry`. The constants below are transcribed from its published `config.json`, and the official `transformers.GraniteForCausalLM` is checked against them.

## At a glance

| | |
| - | - |
| Model key | `ibm-granite/granite-4.2-3b` |
| Parameters (text model) | 3,659,737,600 |
| Layers | 40 (40 full attention) |
| Hidden size | 2,560 |
| MLP width | 8,192 (silu) |
| Vocabulary | 100,352 |
| Norm | `w·x̂`, ε = 1e-05 |
| Embedding | separate from the LM head |
| Logits | no soft-capping |
| Hugging Face class | `GraniteForCausalLM` |
| Shape domain | `T` ∈ \[1, 131,072] tokens, `B` ∈ \[1, 256] sequences, `S` ∈ \[1, 131,072] cached positions, page size 16 |

## What to watch for

* Every layer is full causal attention: 40 query heads, 8 KV heads (5 query heads per KV head), head dim 64.
* The attention scale is the checkpoint's `attention_multiplier`, 1/64, not 1/√64.
* No q/k norms. RMSNorm weights are applied as `w`, with ε = 1e-5.
* RoPE over the full head, θ = 10,000,000. The language-model head is separate from the embedding.

## Compute-graph nodes

Use these paths in Spec Keys: `ibm-granite/granite-4.2-3b@1.0:layers[*].<node>` for per-layer nodes, `ibm-granite/granite-4.2-3b@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 40 | `y[t,i] = x[t,i] / √(Σⱼ x[t,j]² / H + ε) · w[i]` | H=2560, eps=1e-05 |
| `attn.qkv_proj` | `linear` | all 40 | `y[t,n] = Σₖ x[t,k] · w[n,k]` | K=2560, N=3584 |
| `attn.rope` | `rope` | all 40 | `rotate pairs (i, i + 32) by pos · θ^(-2i/64), i < 32; coordinates ≥ 64 unchanged` | D=64, active=32, denom=64, rot=64, theta=10000000 |
| `attn.core` | `decodeGQA` | all 40 | `o[b,h] = Σ_{s < seq_lens[b]} softmax_s(1/64 · ⟨q[b,h], k[b,s,h / 5]⟩) · v[b,s,h / 5]` | D=64, heads=40, kv\_heads=8, scale=1/64 |
| `attn.o_proj` | `linear` | all 40 | `y[t,n] = Σₖ x[t,k] · w[n,k]` | K=2560, N=2560 |
| `attn_residual` | `residual` | all 40 | `y = x + h` | H=2560, layer\_scalar=False, r=1 |
| `post_attn_norm` | `rmsnorm` | all 40 | `y[t,i] = x[t,i] / √(Σⱼ x[t,j]² / H + ε) · w[i]` | H=2560, eps=1e-05 |
| `mlp.gate_up` | `linear` | all 40 | `y[t,n] = Σₖ x[t,k] · w[n,k]` | K=2560, N=16384 |
| `mlp.act` | `siluMul` | all 40 | `y[t,i] = silu(gate_up[t,i]) · gate_up[t,8192+i]` | I=8192, act=silu |
| `mlp.down` | `linear` | all 40 | `y[t,n] = Σₖ x[t,k] · w[n,k]` | K=8192, N=2560 |
| `mlp_residual` | `residual` | all 40 | `y = x + h` | H=2560, layer\_scalar=False, r=1 |
| `final_norm` | `rmsnorm` | — | `y[t,i] = x[t,i] / √(Σⱼ x[t,j]² / H + ε) · w[i]` | H=2560, eps=1e-05 |
| `lm_head` | `lmHead` | — | `z = x wᵀ` | mul=1, tied=False |

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, 2560] |
| `input_norm` | `x` \[T, 2560], `y` \[T, 2560] |
| `attn.qkv_proj` | `x` \[T, 2560], `y` \[T, 3584] |
| `attn.rope` | `q` \[T, 40, 64], `k` \[T, 8, 64], `pos` \[T], `q_out` \[T, 40, 64], `k_out` \[T, 8, 64] |
| `attn.core` | `q` \[B, 40, 64], `k` \[B, S, 8, 64], `v` \[B, S, 8, 64], `seq_lens` \[B], `o` \[B, 40, 64] |
| `attn.o_proj` | `x` \[T, 2560], `y` \[T, 2560] |
| `attn_residual` | `x` \[T, 2560], `h` \[T, 2560], `y` \[T, 2560] |
| `post_attn_norm` | `x` \[T, 2560], `y` \[T, 2560] |
| `mlp.gate_up` | `x` \[T, 2560], `y` \[T, 16384] |
| `mlp.act` | `gate_up` \[T, 16384], `y` \[T, 8192] |
| `mlp.down` | `x` \[T, 8192], `y` \[T, 2560] |
| `mlp_residual` | `x` \[T, 2560], `h` \[T, 2560], `y` \[T, 2560] |
| `final_norm` | `x` \[T, 2560], `y` \[T, 2560] |
| `lm_head` | `x` \[T, 2560], `logits` \[T, 100352] |

## Conformance

The official `transformers.GraniteForCausalLM` agrees with this spec, layer by layer in float64, to a maximum relative error of **2.3e-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 **5.1e-15** on a real prompt (121.8 s).

```bash theme={"system"}
theformalera-conformance verify ibm-granite/granite-4.2-3b                    # the official implementation
theformalera-conformance verify ibm-granite/granite-4.2-3b path/to/model.py   # your implementation
theformalera-conformance spec ibm-granite/granite-4.2-3b                      # the architecture, as Lean derives it
```

## Published configuration

> [accordion] The hyperparameters as the spec renders them (config.json form)
>
> ```json theme={"system"}
> {
>   "vocab_size": 100352,
>   "tie_word_embeddings": false,
>   "rope_theta": 10000000,
>   "rope_parameters": {
>     "rope_type": "default",
>     "rope_theta": 10000000
>   },
>   "rms_norm_eps": 1e-05,
>   "residual_multiplier": 1,
>   "num_key_value_heads": 8,
>   "num_hidden_layers": 40,
>   "num_attention_heads": 40,
>   "mlp_bias": false,
>   "logits_scaling": 1,
>   "intermediate_size": 8192,
>   "hidden_size": 2560,
>   "hidden_act": "silu",
>   "embedding_multiplier": 1,
>   "attention_multiplier": 0.015625,
>   "attention_bias": false,
>   "architectures": [
>     "GraniteForCausalLM"
>   ]
> }
> ```


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