theformalera-conformance verify-all (transformers 5.22, PyTorch 2.15, Lean 4.35, on a CPU):
Published checkpoints
The weight-level cross-check loads the published checkpoint and evaluates the full-size spec with the oracle on a real prompt: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 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.