Skip to main content
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.

​
The checks

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

Verify your implementation

What your implementation must expose, and how to read a failure.

Results for the official implementations

All eight models, measured.