Self-hosting overview - The Formal Era

A Spec Hub is an object store plus an API. The same code serves every setup; only the store and the queue change.

Setup	Store	API	Solving	For
Directory mirror	a directory, read through `file://`	none: the CLI reads the directory	`runner = "local"`	Development, air-gapped CI, offline mirrors
Local API server	a directory	`theformalera-hub serve`	`theformalera-hub worker`	A team Hub on one machine
AWS	S3 + DynamoDB + SQS	Lambda behind CloudFront	ECS Fargate workers	Production

What is in a store

Key prefix	Contents
`packages/<org>/<model>/`	Package archives (`<version>.tgz`), manifests (`<version>.json`) and the version index
`models.json`, `keys.json`, `advisories.json`	The model list, publisher public keys, security advisories
`requests/`, `jobs/`, `queue.json`	Cloud verification requests, jobs and (directory stores) the queue
`lemmas/public/`, `lemmas/orgs/<org>/`	Lemma records and their op index
`lemmas/inbox/`	Deposits waiting for admission
`lemmas/usage/`, `lemmas/open-goals/`	Hit statistics and open goals
`tokens.json`	Token hashes (directory stores; AWS uses DynamoDB)

Operations checklist

Generate a publisher key once, and keep it in a secret store: theformalera-hub keygen.
Publish the specs: theformalera-hub publish. See Publish specs.
Issue tokens: theformalera-hub token (directory) or the Tokens table (AWS).
Run the lemma admission task on a schedule: theformalera-hub lemmas admit. See Lemma administration.
Render and publish the website: theformalera-hub site.

⌘I