Spec packages

Each model’s spec is published as a spec package: a Lean 4 (Lake) workspace plus a manifest, content-addressed and signed.

Part	Contents
Lean sources	The `TheFormalEra` library: Op Specs, the model’s family and registry entry, the compute graph, the oracle, the engine’s semantics and proof library, the built-in lemmas, and `Audit.lean`
Manifest (`theformalera.spec-package/v1`)	Key, version, `spec_version`, scope, architecture summary, the configuration in `config.json` form, nodes, value-flow graph, shape and value domains, audited theorems, trust status, file digests, Lean toolchain
Signature	Ed25519 over the package digest, with the publisher’s key id

The manifest is what theformalera spec show, scan and coverage read; the Lean sources are what proofs are checked against. Fetch a manifest from the API:

curl -s https://hub.theformalera.com/v1/specs/Qwen/Qwen3.8-27B/1.0.0 | jq '{key, version, spec_version, scope, trust}'

{
  "key": "Qwen/Qwen3.8-27B",
  "version": "1.0.0",
  "spec_version": "1.0",
  "scope": "text-only language-model path; the vision encoder and the MTP head are out of scope",
  "trust": {
    "conformance_proof": "pending (Phase 1: reference implementation export via torch.export)",
    "public_audit": "https://hub.theformalera.com/specs/Qwen/Qwen3.8-27B",
    "publisher_verified": true,
    "weight_cross_check": { "status": "not run" }
  }
}

trust.weight_cross_check is filled in from a theformalera-conformance verify-all report when the publisher passes one with --conformance.

Versions

version is the full semver (1.0.0). Spec Keys use spec_version (1.0).
Patch releases change docs and metadata only, never definitions. Minor releases add nodes or optional domains. Major releases change semantics.
Published versions are immutable. A wrong spec is fixed by a new version plus a security advisory for the affected ones; pull warns projects that lock an affected version.

Locking

theformalera pull writes, for each model, the exact version, the package digest, the Lean toolchain and the publisher into theformalera.lock. On every later pull:

the downloaded package’s digest must equal the lock’s, or the command stops (downloaded package digest … does not match …);
the signature is checked against the Hub’s published keys (/v1/keys);
the package is installed into ~/.cache/theformalera/specs/<digest>, which is immutable and shared between projects.

Every result records the spec digest it was verified against, and the release certificate records it again.

CLI

Configuration

Formats

Contents

Versions

Locking

​Contents

​Versions

​Locking

Contents

Versions

Locking