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

# Publish specs

> Build, audit, sign and publish spec packages to a Hub store.

```bash theme={"system"}
uv run theformalera-hub publish \
    --specs specs \
    --store s3://<StoreBucket> \
    --version 1.0.0 \
    --key publisher.pem \
    --conformance conformance-report.json
```

```text theme={"system"}
published  Qwen/Qwen3-0.6B@1.0.0  sha256:96fd971256defe9045d11d0cfeb33f0b32ff47419d8123b0b2c172c42dac5ac1
published  Qwen/Qwen3.8-27B@1.0.0  sha256:313a42af237f0db7ec729fd0d5d9230d932d829da0cbda0c43bdb4d310aaddf4
published  google/gemma-4-12B@1.0.0  sha256:6204c6466455d92cd9e4cf550f8179e48f10045a5dc436f6fd5d86608582418b
published  google/gemma-4-31B@1.0.0  sha256:f54282b3dce7ae04bf106ad67e0553afbfe9ef274fe02530a3b939acf1d76562
published  ibm-granite/granite-4.2-3b@1.0.0  sha256:39f622ebf2401e1bd54076db4f7261ec124141393bcf2628974340a192fc4842
published  ibm-granite/granite-4.2-8b@1.0.0  sha256:69f75bccd199d72da1e58245c866e682ca1c02fe4116eacf0afb477e41873d22
published  ibm-granite/granite-4.2-30b@1.0.0  sha256:f56d0fe066e2555808dafb9d18e82becdb2e6751413a11191f5d00040bec87f8
published  meta-models/Muse-Glimmer-30B@1.0.0  sha256:da2208d29ea76be75817731b4b1f7081a0d41e274bc724929f759c2d0f7246d0
```

## What `publish` does

**1. Build**

`lake build` compiles the library and checks every proof. `--skip-build` skips this when the workspace is already built.

**2. Audit**

`Audit.lean` lists the main theorems and their axioms. Publishing fails if any of them uses anything beyond `propext`, `Classical.choice` and `Quot.sound`.

**3. Export**

For every model (or only those given with `--model`), `theformalera-spec` exports the nodes, the value-flow graph, the shape and value domains, the configuration in `config.json` form and the architecture summary into the manifest.

**4. Attach trust status**

With `--conformance`, the result of a `theformalera-conformance verify-all --report` run is recorded for each model.

**5. Sign and store**

Each package is signed with the publisher key and written with its manifest, its version index entry and the model list. Its public key is added to `keys.json`.

Packages are immutable. Publishing an existing version with **different** content is refused; with identical content it prints `unchanged`. To change a spec, bump the version. Patch versions may change only docs and metadata.

## After publishing a new library version

The engine's certificates import the spec library's Lean modules, including its built-in lemmas. Projects pick up a new package with `theformalera pull --update`.

If you add Lean lemmas that certificates use, republish the package. An older package lacks them, and proofs that need them fail to check against it.

## Advisories

When a published spec turns out to be wrong:

```bash theme={"system"}
uv run theformalera-hub advisory --store s3://<StoreBucket> --id TFE-2026-001 \
    --key Qwen/Qwen3.8-27B --versions 1.0.0 --summary "attn.gate applied before o_proj" --fixed 1.0.1
```

Every project that locks an affected version is warned on its next `pull`, and nightly CI runs report it.


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