Verify your implementation

theformalera-conformance verify <model key> [implementation] [options]

<model key> is one of the supported models; 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.

Hugging Face compatible
Adapter

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

qwen3_minimal.py

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.

For an implementation with its own parameter names or calling convention, define module-level functions:

my_model_adapter.py

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 <key> --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:

qwen3_5_bug_gate.py

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

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:

theformalera-conformance verify Qwen/Qwen3-0.6B examples/conformance/implementations/qwen3_bug_rope.py --skip-proofs

 ✓   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

theformalera-conformance verify Qwen/Qwen3-0.6B impl.py --report report.json

{
  "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}}
  ]
}

Get started

Concepts

Guides

Model conformance

Case studies

Help

Verify your implementation

What the implementation must provide

Options

Reading a failure

Other failures

JSON report

​What the implementation must provide

​Options

​Reading a failure

​Other failures

​JSON report

What the implementation must provide

Options

Reading a failure

Other failures

JSON report