> ## 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. # Model conformance > Check that a PyTorch implementation of a whole model computes exactly what its Lean 4 Model Spec says. Kernel verification proves that a kernel equals a spec node. **Model conformance** checks the other link in the chain: that a PyTorch implementation of the *whole model* computes what the Lean 4 Model Spec says, layer by layer. `theformalera-conformance` serves two purposes: 1. **Trust in the specs.** The official Hugging Face implementation of every supported model is checked against its spec, so "is the spec right?" becomes "does the spec equal the official implementation?". 2. **Verify your own implementation.** Pass any PyTorch implementation of a supported model (a from-scratch rewrite, a port, an agent-generated model) and get the same verdict, with the first layer at which it disagrees. ```bash theme={"system"} theformalera-conformance verify Qwen/Qwen3-0.6B examples/conformance/implementations/qwen3_minimal.py ``` ```text theme={"system"} ╭────────────────────────────────────────────────────────────────────────────────────────╮ │ The Formal Era formal verification of a model implementation │ ╰────────────────────────────────────────────────────────────────────────────────────────╯ model Qwen/Qwen3-0.6B implementation Qwen3ForCausalLM examples/conformance/implementations/qwen3_minimal.py profile reduced-width configuration of the same architecture · 2 weight draws · lengths [7, 12] · float64 ────────────────────────────────────────────────────────────────────────────────────────── ✓ Proofs 37/37 theorems checked by the Lean kernel, no sorry 4.1 s ✓ Configuration 17 hyperparameters match config.json 502 ms ✓ Interface 46 tensors, names and shapes match the specification 0 ms ✓ Conformance 4 runs agree with the specification (max rel. err 1.5e-15 ≤ 1e-09) 131 ms ✓ Causality prefix logits unaffected by 11 suffix perturbations (max rel. change 0.0e+00) 24 ms seed tokens per-layer agreement (embed → last layer) logits rel. err 0 7 █████ 7.9e-16 0 12 █████ 9.6e-16 1 7 █████ 6.9e-16 1 12 █████ 7.0e-16 ┏━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┓ ┃ ✓ VERIFIED Qwen3ForCausalLM implements Qwen/Qwen3-0.6B as specified ┃ ┗━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┛ ``` ## The checks | Check | What it establishes | | - | - | | **Proofs** | The Lean spec library builds and its 37 theorems are kernel-checked with standard axioms only (no `sorry`). | | **Configuration** | Every hyperparameter of the spec equals the value in the checkpoint's published `config.json`, or the value Hugging Face resolves when the file relies on a default. | | **Interface** | The implementation's parameters are exactly the spec's tensors: same names, same shapes. Nothing missing, nothing extra. | | **Conformance** | On random weights and random token sequences, every residual stream (embedding output, after each layer, after the final norm) and the logits agree with the Lean oracle. | | **Causality** | Changing a suffix of the input never changes earlier logits, the property proved for the spec in `TheFormalEra.forward_causal`. | | **Pretrained** *(opt-in)* | The same agreement on the published checkpoint's weights and a real prompt, with the full-size configuration. | ## How the comparison works **1. Draw weights from the spec's manifest** The spec lists every parameter tensor with its shape and an init kind (`linear`, `embedding`, `norm_scaled`, `norm_offset`, …). Weights are drawn so that activations stay O(1) through the network. Norm weights are perturbed away from their identity value, so a wrong formula cannot hide behind `w = 1`. **2. Evaluate the spec with the Lean oracle** `theformalera-spec oracle` evaluates the Model Spec in binary64. Its evaluators are proved equal to the spec definitions (`runTrace_fst`, `linear_eq_linearPar`, `seqMap_eq_seqMapPar`). **3. Run the implementation in float64** The implementation is built and run with float32 requests promoted to float64: tensors created as `float32`, `.float()`, `.to(torch.float32)`, `softmax(…, dtype=float32)`. That way both sides evaluate the same real-number expression, up to rounding and summation order. **4. Compare every block** For each tensor, the relative error `max |impl − spec| / max |spec|` must be at most `--rtol` (default `1e-9`). A failure reports the **first** block that disagrees: every earlier block agrees with the spec, so the bug is in that block. > [!NOTE] > > Floating-point non-associativity is disregarded by design. Measured agreement for correct implementations is around `1e-15`; a real bug shows up at `1e-6` (a misplaced ε) to `1e0` (a wrong head mapping). ## The reduced-width profile By default, conformance uses a **reduced-width** configuration of the same architecture. It has the same layer-type pattern, attention variants, norms, RoPE variant and multipliers, at a small width (hidden size 64–160, 4–8 layers, vocabulary 512). The theorem `reduced_same_architecture` proves the correspondence for every model. So a run takes seconds, even for 30B architectures. * `--full` uses the full-size configuration on random weights. * `--pretrained` also loads the published checkpoint and compares on a real prompt. Both hold the model in float64, about 8 bytes per parameter: 5 GB for Qwen3-0.6B, about 250 GB for a 30B model. ## Next > [card] [Verify your implementation](https://docs.theformalera.com/conformance/verify-an-implementation.md) > > What your implementation must expose, and how to read a failure. > [card] [Results for the official implementations](https://docs.theformalera.com/conformance/results.md) > > All eight models, measured. This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.