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

# Self-hosting overview

> Run your own Spec Hub: a directory mirror, a local API server, or the AWS deployment.

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](https://docs.theformalera.com/self-hosting/local-hub.md) | a directory, read through `file://` | none: the CLI reads the directory | `runner = "local"` | Development, air-gapped CI, offline mirrors |
| [Local API server](https://docs.theformalera.com/self-hosting/local-hub.md#run-the-api) | a directory | `theformalera-hub serve` | `theformalera-hub worker` | A team Hub on one machine |
| [AWS](https://docs.theformalera.com/self-hosting/aws.md) | S3 + DynamoDB + SQS | Lambda behind CloudFront | ECS Fargate workers | Production |

```mermaid theme={"system"}
flowchart LR
  specs["specs/ (Lean 4)"] -->|"theformalera-hub publish<br/>build · audit · sign"| store[("Store<br/>packages · lemmas<br/>jobs · cache")]
  store --> api["API<br/>/v1/specs · /v1/verify · /v1/lemmas"]
  api --> cli["theformalera CLI"]
  api -->|queue| worker["Solve workers<br/>(engine + Lean)"]
  worker --> store
  store -->|"lemmas admit<br/>(scheduled)"| store
```

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

1. Generate a publisher key once, and keep it in a secret store: `theformalera-hub keygen`.
2. Publish the specs: `theformalera-hub publish`. See [Publish specs](https://docs.theformalera.com/self-hosting/publish-specs.md).
3. Issue tokens: `theformalera-hub token` (directory) or the `Tokens` table (AWS).
4. Run the lemma admission task on a schedule: `theformalera-hub lemmas admit`. See [Lemma administration](https://docs.theformalera.com/self-hosting/lemma-administration.md).
5. Render and publish the website: `theformalera-hub site`.


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