> ## 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. # Verify your implementation > Point the conformance verifier at a PyTorch file, and read where it disagrees with the spec. ```bash theme={"system"} theformalera-conformance verify [implementation] [options] ``` `` is one of the [supported models](https://docs.theformalera.com/models/index.md); `theformalera-conformance models` lists them. Without an implementation argument, the official Hugging Face class is checked. ## What the implementation must provide The implementation is a Python file (`path/to/model.py`, optionally `:Name`) or a module path (`package.module:attr`). It can be written in either of two styles. > [tab] Hugging Face compatible > > An `nn.Module` subclass that: > > * is constructible as `cls(config)` from a `transformers` configuration; > * uses Hugging Face parameter names in `state_dict()` (`model.layers.0.self_attn.q_proj.weight`, …); > * returns logits from `forward(input_ids=...)`: a tensor, a dict with `"logits"`, or an object with `.logits`. > > Expose it as `MODEL_CLASS`, or define exactly one class whose name ends in `ForCausalLM` or `ForConditionalGeneration`. > > For **layer-by-layer** localisation, also accept `output_hidden_states=True` and return `hidden_states`: the embedding output first, then one tensor per layer, with the last one taken **after** the final norm (the Hugging Face convention). > > ```python qwen3_minimal.py theme={"system"} > class Qwen3ForCausalLM(nn.Module): > def __init__(self, config): > super().__init__() > self.model = Decoder(config) > self.lm_head = nn.Linear(config.hidden_size, config.vocab_size, bias=False) > if config.tie_word_embeddings: > self.lm_head.weight = self.model.embed_tokens.weight > > def forward(self, input_ids: torch.Tensor, output_hidden_states: bool = False, **_): > x = self.model.embed_tokens(input_ids) > hidden = [x] > for layer in self.model.layers: > x = layer(x) > hidden.append(x) > x = self.model.norm(x) > hidden[-1] = x # Hugging Face convention: the last hidden state is normalised > logits = self.lm_head(x) > return {"logits": logits, "hidden_states": hidden} if output_hidden_states else logits > > > MODEL_CLASS = Qwen3ForCausalLM > ``` > > The complete file is about 100 lines and has no dependency on `transformers` modeling code: `examples/conformance/implementations/qwen3_minimal.py`. > [tab] Adapter > > For an implementation with its own parameter names or calling convention, define module-level functions: > > ```python my_model_adapter.py theme={"system"} > NAME = "my-model" # optional display name > > def build(config): # required: a transformers config -> nn.Module > return MyModel.from_hf_config(config) > > def load_weights(model, tensors): # optional: tensors keyed by the spec's names > model.tok_emb.weight.copy_(tensors["embed_tokens.weight"]) > for i, blk in enumerate(model.blocks): > blk.wq.weight.copy_(tensors[f"layers.{i}.self_attn.q_proj.weight"]) > ... > > def hidden_states(model, input_ids): # optional: (residual streams, logits) for localisation > return model.forward_with_trace(input_ids) > ``` > > Spec names are relative to the decoder root (`embed_tokens.weight`, `layers.0.self_attn.q_proj.weight`, …, plus `lm_head.weight` when it is not tied). `theformalera-spec manifest --reduced` prints the full list with shapes. > > `build` can also wrap the official class and patch one module. This is how the bug examples are written: > > ```python qwen3_5_bug_gate.py theme={"system"} > def build(config): > model = transformers.Qwen3_5ForConditionalGeneration(config) > for layer in model.model.language_model.layers: > ... # replace self_attn with SwappedGateAttention in the full-attention layers > return model > ``` > [!NOTE] > > The implementation is built and run on the CPU, in float64, with every float32 request promoted to float64. Do not hard-code `torch.float32` or `bfloat16` casts that cannot be promoted, such as dtype arguments to custom CUDA ops. ## Options | Option | Default | Meaning | | - | - | - | | `--full` | off | Use the full-size configuration instead of the reduced-width one | | `--pretrained` | off | Also compare on the published checkpoint (downloaded from Hugging Face) | | `--prompt TEXT` | `The capital of France is` | Prompt for `--pretrained`; repeatable | | `--seeds N` | `2` | Number of random weight draws | | `--length N` | `7`, `12` | Token sequence lengths; repeatable | | `--rtol X` | `1e-9` | Agreement threshold (maximum relative error per tensor) | | `--skip-proofs` | off | Do not rebuild and re-audit the Lean library | | `--report FILE` | — | Write a JSON report | The exit status is 0 only for **VERIFIED**. ## Reading a failure This implementation applies RoPE to interleaved pairs (GPT-J style) instead of rotate-half: ```bash theme={"system"} theformalera-conformance verify Qwen/Qwen3-0.6B examples/conformance/implementations/qwen3_bug_rope.py --skip-proofs ``` ```text theme={"system"} ✓ Configuration 17 hyperparameters match config.json 1.2 s ✓ Interface 46 tensors, names and shapes match the specification 0 ms ✗ Conformance disagreement from layer 0 (seed 0, length 7, rel. err 5.6e-01) 248 ms ✓ Causality prefix logits unaffected by 11 suffix perturbations (max rel. change 0.0e+00) 99 ms seed tokens per-layer agreement (embed → last layer) logits rel. err 0 7 █████ 3.1e-01 0 12 █████ 3.5e-01 1 7 █████ 3.8e-01 1 12 █████ 2.6e-01 ┏━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┓ ┃ ✗ NOT VERIFIED Qwen3ForCausalLM deviates from the specification of Qwen/Qwen3-0.6B ┃ ┃ • Conformance: disagreement from layer 0 (seed 0, length 7, rel. err 5.6e-01) ┃ ┃ first divergence: layer 0 — every earlier block agrees with the specification ┃ ┗━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┛ ``` In the terminal, the per-layer bar is green for blocks within `1e-12`, yellow up to `1e-9`, and red above. "First divergence: layer 0" means the embedding agrees and layer 0 is the first block that does not, so the bug is inside the decoder layer. The bundled examples, all against the reduced profile: | Implementation | Bug | Verdict | | - | - | - | | `qwen3_minimal.py` | none | ✓ VERIFIED, max rel. err 1.5e-15 | | `qwen3_bug_rope.py` | RoPE on interleaved pairs instead of rotate-half | ✗ from layer 0, rel. err 5.6e-01 | | `qwen3_bug_eps.py` | RMSNorm ε added outside the square root | ✗ from layer 0, rel. err 1.0e-06 | | `qwen3_bug_gqa.py` | KV heads repeated with `repeat` instead of `repeat_interleave` | ✗ from layer 0, rel. err 1.1e+00 | | `qwen3_bug_qknorm.py` | q/k norm applied after RoPE instead of before | ✗ from layer 0, rel. err 1.2e-01 | | `qwen3_5_bug_gate.py` (Qwen3.8-27B) | Fused q/gate projection split in the wrong order | ✗ from **layer 3**, rel. err 6.8e-01 | The last row shows localisation working in a hybrid model. Layers 0–2 are Gated DeltaNet and agree with the spec; layer 3 is the first full-attention layer, where the gate is used. A misplaced ε changes the result by only `1e-6`, which a `torch.allclose` test would pass. It is still a different function, and it fails at the default `rtol` of `1e-9`. ## Other failures | Check | Typical message | Meaning | | - | - | - | | Configuration | `2 mismatches` and `field: spec … ≠ config …` | The spec's hyperparameters differ from `config.json`. This is a spec problem, not an implementation problem. | | Interface | `missing 2, unexpected 1, wrong shape 0` | Parameter names or shapes differ from the spec; the missing and extra names are listed. | | Interface | `cannot construct the implementation: …` | `build(config)` or `cls(config)` raised. | | Conformance | `error while running the implementation: …` | The forward pass raised. | | Causality | `prefix logits unaffected …` fails | A position attends to later tokens: a mask bug. | ## JSON report ```bash theme={"system"} theformalera-conformance verify Qwen/Qwen3-0.6B impl.py --report report.json ``` ```json theme={"system"} { "key": "Qwen/Qwen3-0.6B", "implementation": "Qwen3ForCausalLM", "profile": "reduced", "ok": true, "checks": [ {"name": "config", "ok": true, "detail": "17 hyperparameters match config.json", "seconds": 0.5, "data": {…}}, {"name": "conformance", "ok": true, "detail": "4 runs agree with the specification (max rel. err 1.5e-15 ≤ 1e-09)", "seconds": 0.13, "data": {"trials": […], "worst": 1.5e-15, "first_bad": null}} ] } ``` This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.