Local Hub - The Formal Era

A directory mirror

uv run theformalera-hub keygen -o publisher.pem
uv run theformalera-hub publish --specs specs --store hub-data --version 1.0.0 --key publisher.pem

Point projects at it with THEFORMALERA_HUB (or hub = "file:///…" in theformalera.toml):

export THEFORMALERA_HUB=file://$PWD/hub-data
export THEFORMALERA_MATHLIB=$PWD/specs        # reuse this workspace's Mathlib build
cd examples/acme-qwen3.8-27b-h100 && theformalera pull && theformalera verify

With a file:// Hub:

no token is needed; THEFORMALERA_ORG names your organisation (default local-org) and THEFORMALERA_PLAN your plan (default enterprise);
the lemma libraries are directories in the store; deposits go to lemmas/inbox/ and are admitted by theformalera-hub lemmas admit;
cloud verification is not available: use runner = "local".

theformalera.lock pins package digests. A lock written against one Hub only works with a Hub that serves the same package. After pointing a project at a different Hub, run theformalera pull --update, or delete the lock and pull again.

Run the API

uv run theformalera-hub serve --store hub-data --host 0.0.0.0 --port 8700

Then set hub = "http://<host>:8700" in projects. Issue tokens with:

uv run theformalera-hub token --store hub-data --tenant acme --plan team

tfe_…

For cloud-style solving, run one or more workers next to it. They take jobs from the store’s queue and run the engine:

uv run theformalera-hub worker --store hub-data --specs specs

Render the website

uv run theformalera-hub site --store hub-data -o site
uv run python -m http.server -d site 8080

The site has a page per model (Lean definitions, rendered formulas, the compute graph and the trust status), a page per node, and a page per lemma.

​A directory mirror

​Run the API

​Render the website

A directory mirror

Run the API

Render the website