Write and check a spec

Most users never write a spec: the Model Specs on Spec Hub are written by us or by model vendors. Read this page if you need a spec for a model that is not on the Hub yet, or a private spec for an unreleased model.

Draft from a reference implementation

theformalera spec new --from-export model.pt2 --name Acme.MyModel -o Draft.lean

spec new reads a graph exported with torch.export. It strips engineering nodes (KV-cache updates, device and dtype moves, views that only reorganise memory, backend branches) and maps recognised subgraphs onto Op Specs:

ATen pattern	Op Spec
`pow(x, 2) → mean(-1) → add(eps) → rsqrt → mul(x) → mul(w)`	`rmsnorm` / `rmsnormOffset`
`linear(x, W)`, `mm`, `matmul` with a weight parameter	`linear`
`silu(a) * b`	`siluMul`
`scaled_dot_product_attention`, softmax(QKᵀ)·V	`causalGQA`
`cos`/`sin` tables, `cat(-x2, x1)` rotate-half	`rope`
`embedding`	`embed`

Unrecognised compute nodes are kept as placeholders marked -- REVIEW:. The draft is a starting point: publish it only after a human review and a conformance check.

How models are defined in the library

The spec library (specs/) defines each architecture family as a function from its Hugging Face hyperparameters to a model configuration (ModelCfg). That is where the architecture knowledge lives: which norms, which RoPE variant, which multipliers. specs/TheFormalEra/Spec/Families.lean has five families today: Qwen3Hyper, Qwen35Hyper, GraniteHyper, Gemma4Hyper and MuseHyper. A model is then one record of hyperparameters plus one registry entry (specs/TheFormalEra/Spec/Registry.lean):

def qwen3_0_6b : Qwen3Hyper where
  vocab_size := 151936
  hidden_size := 1024
  intermediate_size := 3072
  num_hidden_layers := 28
  num_attention_heads := 16
  num_key_value_heads := 8
  head_dim := 128
  rms_norm_eps := 1e-6
  rope_theta := 1000000
  tie_word_embeddings := true
  sliding_window := none
  max_window_layers := 28

def qwen3_0_6b_reduced : Qwen3Hyper :=
  { qwen3_0_6b with vocab_size := 512, hidden_size := 64, intermediate_size := 192,
                    num_hidden_layers := 4, num_attention_heads := 16, num_key_value_heads := 8,
                    head_dim := 8, max_window_layers := 4 }

def registry : List ModelEntry := [
  ⟨"Qwen/Qwen3-0.6B", .qwen3 qwen3_0_6b, .qwen3 qwen3_0_6b_reduced, "Qwen3ForCausalLM"⟩,
  …]

Every family also has toHF, which renders the hyperparameters back in config.json form. The conformance check compares that rendering with the published config.json, field by field. To add a checkpoint of an existing family, add its record, a reduced record with the same layer pattern, and a registry entry. To add a new architecture, add a family. The compute graph (TheFormalEra.Models.Graph), the executable oracle and the CLI then pick it up.

The reduced configuration must have the same architecture: the same layer-type pattern, attention variants, norms and multipliers, at a small width. The theorem reduced_same_architecture checks this for every registry entry.

Check a spec package

theformalera spec check specs/

spec check:

runs lake build: the definitions type-check and every proof is checked;
runs the axiom audit (Audit.lean): every listed theorem depends only on propext, Classical.choice and Quot.sound;
exports each model’s graph and checks it is connected: every node input is produced by another node, except the graph’s inputs (tokens, positions, seq_lens) and cache values.

Check it against the reference implementation

theformalera-conformance verify <org>/<model>

This runs the official Hugging Face implementation against your spec, layer by layer, in float64. See Model conformance. The spec and the reference must agree before the spec is published.

Publish

theformalera-hub publish --specs specs --store <store> --version 1.1.0 --key publisher.pem \
    --model <org>/<model> --conformance conformance-report.json

See Publish specs. Published versions are immutable: publishing an existing version with a different digest is refused. Bump the version instead.

Get started

Concepts

Guides

Model conformance

Case studies

Help

Draft from a reference implementation

How models are defined in the library

Check a spec package

Check it against the reference implementation

Publish

​Draft from a reference implementation

​How models are defined in the library

​Check a spec package

​Check it against the reference implementation

​Publish

Draft from a reference implementation

How models are defined in the library

Check a spec package

Check it against the reference implementation

Publish