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

# Results for the official implementations

> Measured conformance of the official Hugging Face implementation of every supported model to its Lean 4 spec.

Every Model Spec on Spec Hub is checked against the official Hugging Face implementation of its model. These are the results of `theformalera-conformance verify-all` (transformers 5.22, PyTorch 2.15, Lean 4.35, on a CPU):

```bash theme={"system"}
theformalera-conformance verify-all
```

```text theme={"system"}
✓ proofs: 37/37 theorems checked by the Lean kernel, no sorry

 model                          cfg   api   spec   causal   max err     time
 ───────────────────────────────────────────────────────────────────────────
 Qwen/Qwen3-0.6B                 ✓     ✓     ✓       ✓      1.5e-15    2.0 s
 Qwen/Qwen3.8-27B                ✓     ✓     ✓       ✓      4.1e-14    3.8 s
 google/gemma-4-12B              ✓     ✓     ✓       ✓      6.7e-16   715 ms
 google/gemma-4-31B              ✓     ✓     ✓       ✓      8.6e-16    1.3 s
 ibm-granite/granite-4.2-3b      ✓     ✓     ✓       ✓      2.3e-15    1.8 s
 ibm-granite/granite-4.2-8b      ✓     ✓     ✓       ✓      1.6e-15    1.6 s
 ibm-granite/granite-4.2-30b     ✓     ✓     ✓       ✓      1.7e-15    1.9 s
 meta-models/Muse-Glimmer-30B    ✓     ✓     ✓       ✓      7.7e-15    2.0 s

cfg: hyperparameters = config.json · api: parameter names/shapes · spec: conformance to the Lean oracle ·
causal: suffix independence
all models verified
```

| Column | Check |
| - | - |
| `cfg` | Every hyperparameter of the spec equals the published `config.json` |
| `api` | The official class's parameters are exactly the spec's tensors |
| `spec` | Every residual stream and the logits agree with the Lean oracle, on 2 weight draws × 2 sequence lengths, reduced-width profile |
| `causal` | Earlier logits never depend on later tokens |
| `max err` | Worst relative error over every compared tensor |

## Published checkpoints

The weight-level cross-check loads the published checkpoint and evaluates the full-size spec with the oracle on a real prompt:

| Model | Parameters | Max rel. err | Next token for "The capital of France is" | Time |
| - | - | - | - | - |
| `Qwen/Qwen3-0.6B` | 0.60 B | 7.7e-15 | spec ` Paris`, implementation ` Paris` | 85.5 s |
| `ibm-granite/granite-4.2-3b` | 3.66 B | 5.1e-15 | spec ` Paris`, implementation ` Paris` | 121.8 s |

```bash theme={"system"}
theformalera-conformance verify Qwen/Qwen3-0.6B --pretrained
```

```text theme={"system"}
 ✓   Pretrained      published checkpoint (0.60 B params), 1 prompt(s): implementation =               85.5 s
                     specification (max rel. err 7.7e-15); “The capital of France is” → spec '
                     Paris', impl ' Paris'
```

> [!NOTE]
>
> The checkpoint cross-check holds the full model in float64, about 8 bytes per parameter. It has been run for the two checkpoints above. For the 12B–31B checkpoints it needs roughly 100–250 GB of memory, and their spec trust rests on the reduced-width conformance plus the configuration check.

## Why a reduced width is enough to catch architecture bugs

The reduced configurations keep everything except the widths: the layer-type pattern, every attention variant (sliding and global, gated, NoPE), the norms, the RoPE variant and the multipliers. `TheFormalEra.reduced_same_architecture` proves this for all eight models. Bugs in the architecture (a wrong norm, a swapped gate, a wrong head mapping, RoPE on the wrong pairs) show up at any width, as the [bug examples](https://docs.theformalera.com/conformance/verify-an-implementation.md#reading-a-failure) show.

What a reduced width cannot catch is a hyperparameter typo, since the widths are different. That is what the **configuration** check is for: the full-size hyperparameters of the spec are compared with `config.json`, field by field.


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