theformalera-hub

 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

theformalera-hub keygen [-o publisher.pem]

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

publish

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:

lake build compiles the library and checks every proof (skipped with --skip-build);
the axiom audit confirms no theorem uses sorry;
each model’s graph, domain, configuration and architecture are exported;
the conformance status from a verify-all report is attached, if given;
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

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

theformalera-hub serve [--store hub-data] [--host 127.0.0.1] [--port 8700]

Run the Hub API with uvicorn, for development or a self-hosted Hub.

worker

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

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

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

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

CLI

Configuration

Formats

keygen

publish

site

serve

worker

token

advisory

lemmas

​keygen

​publish

​site

​serve

​worker

​token

​advisory

​lemmas

keygen

publish

site

serve

worker

token

advisory

lemmas