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

> Operate a Spec Hub: keys, publishing, the API server, the solve worker, tokens, advisories and the Lemma Hub.

```text theme={"system"}
 Usage: theformalera-hub [OPTIONS] COMMAND [ARGS]...

 Spec Hub: publish specs, serve the API and site.
```

`--store` takes a directory (self-hosted, mirrors, development) or `s3://bucket/prefix` (AWS). It defaults to `hub-data`.

## keygen

```bash theme={"system"}
theformalera-hub keygen [-o publisher.pem]
```

Generate an Ed25519 publisher key pair: `publisher.pem` (mode `0600`) and `publisher.pub`. Prints the key id.

## publish

```bash theme={"system"}
theformalera-hub publish [--specs specs] [--store hub-data] [--version 1.0.0] [--key publisher.pem]
                         [--publisher NAME] [--model KEY]... [--conformance report.json] [--skip-build]
```

Build, audit, sign and store the spec package of every model in the Lean workspace:

1. `lake build` compiles the library and checks every proof (skipped with `--skip-build`);
2. the axiom audit confirms no theorem uses `sorry`;
3. each model's graph, domain, configuration and architecture are exported;
4. the conformance status from a `verify-all` report is attached, if given;
5. each package is signed and written with its version index.

Published versions are immutable: publishing the same version with a different digest is refused. A rerun with identical content prints `unchanged`.

| Option | Default | Meaning |
| - | - | - |
| `--version` | `1.0.0` | Package version (semver) |
| `--publisher` | `theformalera (verified)` | Publisher name shown as the badge |
| `--model` | all | Publish only these models; repeatable |

## site

```bash theme={"system"}
theformalera-hub site [--store hub-data] [-o site]
```

Render the static Spec Hub website: model pages with Lean definitions, rendered formulas, compute graphs and trust status, and lemma pages.

## serve

```bash theme={"system"}
theformalera-hub serve [--store hub-data] [--host 127.0.0.1] [--port 8700]
```

Run the [Hub API](https://docs.theformalera.com/api-reference/introduction.md) with uvicorn, for development or a self-hosted Hub.

## worker

```bash theme={"system"}
theformalera-hub worker [--store hub-data] [--specs DIR] [--once]
```

The cloud solve worker: it takes verification jobs from the queue and runs the engine on them. `--specs` is the spec workspace used to check proofs. `--once` processes the queue once and exits.

## token

```bash theme={"system"}
theformalera-hub token [--store hub-data] [--tenant NAME] [--plan team]
```

Issue an API token (`tfe_…`) for a tenant of a self-hosted Hub. Only the token's SHA-256 is stored. The AWS deployment keeps tokens in DynamoDB instead.

## advisory

```bash theme={"system"}
theformalera-hub advisory --store hub-data --id TFE-2026-001 --key Qwen/Qwen3.8-27B \
    --versions 1.0.0 --versions 1.0.1 --summary "…" [--fixed 1.0.2]
```

Publish a spec security advisory. Projects that lock an affected version are warned on their next `pull`.

## lemmas

| Command | Does |
| - | - |
| `lemmas admit --store S --specs DIR [--private-node NODE]...` | Re-check every queued deposit with Lean (template regeneration, axiom allowlist, statement-hash id, dedupe) and admit it; fold usage reports into the hit statistics |
| `lemmas cap --store S --org ORG --cap off\|org\|public` | Set an organisation's contribution cap |
| `lemmas audit --store S --org ORG` | Print the organisation's audit log of lemma uploads (JSON lines) |
| `lemmas snapshot --store S [--org ORG]` | Record a snapshot of the libraries; projects pin it with `[lemmas] snapshot` |
| `lemmas migrate --store S --specs DIR` | Re-check every lemma against the workspace's toolchain; failures become `pending-migration` and leave retrieval |
| `lemmas stats --store S [--org ORG]` | Library sizes by scope, hits and open goals |

```text theme={"system"}
$ theformalera-hub lemmas admit --store "$HUB_STORE" --specs "$THEFORMALERA_MATHLIB"
usage: folded 3 verification report(s) into the hit statistics
D-76ec659a2f (acme): 1 admitted, 0 rejected, 0 duplicates
  + L-d07f2c  general-level → org  (Lean re-check 2.32s)
```

See [Lemma administration](https://docs.theformalera.com/self-hosting/lemma-administration.md).


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