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

# Spec packages

> What a published spec package contains, how it is versioned, signed and locked.

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

## Contents

| 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](https://docs.theformalera.com/api-reference/introduction.md):

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

```json theme={"system"}
{
  "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](https://docs.theformalera.com/api-reference/introduction.md) 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.


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