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

# theformalera-conformance

> models, spec, prove, verify and verify-all.

```text theme={"system"}
 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

```bash theme={"system"}
theformalera-conformance models
```

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

```text theme={"system"}
 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

```bash theme={"system"}
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

```bash theme={"system"}
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

```bash theme={"system"}
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](https://docs.theformalera.com/conformance/verify-an-implementation.md).

## verify-all

```bash theme={"system"}
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](https://docs.theformalera.com/conformance/results.md).


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.