theformalera-conformance

 Usage: theformalera-conformance [OPTIONS] COMMAND [ARGS]...

 Check PyTorch implementations of language models against the Lean 4 model specs of Spec Hub.

The commands use the Lean spec library in specs/ (or $THEFORMALERA_SPECS) and its theformalera-spec executable. lake is looked up on PATH, then in ~/.elan/bin.

models

theformalera-conformance models

The supported model keys, as the Lean spec defines them:

 model key                      layers    params   architecture
 ────────────────────────────────────────────────────────────────────────────────────────────────────
 Qwen/Qwen3-0.6B                    28    0.60 B   attention
 Qwen/Qwen3.8-27B                   64   26.90 B   48 deltanet + 16 global, gated attn
 google/gemma-4-12B                 48   11.91 B   40 local + 8 global, sandwich norms, softcap 30, attn
                                                   scale 1, embed × √3840
 google/gemma-4-31B                 60   30.70 B   50 local + 10 global, sandwich norms, softcap 30, attn
                                                   scale 1, embed × √5376
 ibm-granite/granite-4.2-3b         40    3.66 B   attention, attn scale 1/64
 ibm-granite/granite-4.2-8b         40    8.79 B   attention, attn scale 1/128
 ibm-granite/granite-4.2-30b        64   29.28 B   attention, attn scale 1/128
 meta-models/Muse-Glimmer-30B       52   27.85 B   39 local + 13 global, gated attn, NoPE, sandwich norms,
                                                   softcap 20, logit multiplier

spec

theformalera-conformance spec KEY [--reduced]

The architecture tree of a Model Spec, derived by Lean. --reduced shows the reduced-width configuration used by default for conformance.

prove

theformalera-conformance prove

Build the Lean library and the oracle, then audit every theorem: each is listed with its statement, and the command exits 0 only if all of them depend on standard axioms only.

verify

theformalera-conformance verify KEY [IMPLEMENTATION] [--full] [--pretrained] [--prompt TEXT]...
                                    [--seeds N] [--length N]... [--rtol X] [--skip-proofs] [--report FILE]

Argument / option	Default	Meaning
`KEY`	required	A supported model key
`IMPLEMENTATION`	the official Hugging Face class	`path/to/model.py[:Name]` or `package.module:attr`
`--full`	off	Full-size configuration instead of the reduced-width one
`--pretrained`	off	Also compare on the published checkpoint
`--prompt`	`The capital of France is`	Prompt for `--pretrained`; repeatable
`--seeds`	`2`	Random weight draws
`--length`	`7`, `12`	Sequence lengths; repeatable
`--rtol`	`1e-9`	Maximum relative error per compared tensor
`--skip-proofs`	off	Skip the Lean build and audit
`--report`	—	Write a JSON report

See Verify your implementation.

verify-all

theformalera-conformance verify-all [--skip-proofs] [--seeds N]

Verify the official Hugging Face implementation of every supported model, and print one row per model. See Results.

CLI

Configuration

Formats

models

spec

prove

verify

verify-all

​models

​spec

​prove

​verify

​verify-all

models

spec

prove

verify

verify-all