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

# Spec Hub API

> The HTTP API behind theformalera: the spec registry, cloud verification and the Lemma Hub.

The `theformalera` CLI is the main client of this API. You need it directly only to build your own tooling, a dashboard, or a mirror.

| Base URL | |
| - | - |
| `https://hub.theformalera.com` | The hosted Spec Hub |
| `http://127.0.0.1:8700` | A local Hub started with `theformalera-hub serve` |

All endpoints are under `/v1` and exchange JSON, except the package download.

## Authentication

```bash theme={"system"}
curl -H "Authorization: Bearer $THEFORMALERA_TOKEN" https://hub.theformalera.com/v1/whoami
```

```json theme={"system"}
{ "user": "acme", "tenant": "acme", "plan": "team" }
```

| Group | Token |
| - | - |
| Registry (`/v1/models`, `/v1/specs/…`, `/v1/advisories`, `/v1/keys`, `/v1/health`) | not needed |
| Verification (`/v1/whoami`, `/v1/verify`, `/v1/jobs/…`, `/v1/cache/lookup`) | required |
| Lemma Hub reads (`/v1/lemmas/prefetch`, `/v1/lemmas`, `/v1/lemmas/{id}`) | optional; without one, only the public library is visible |
| Lemma Hub writes and policy (`/v1/lemmas/deposit`, `/v1/lemmas/usage`, `/v1/orgs/{org}/lemma-policy`) | required |

Tokens look like `tfe_…`. The Hub stores only their SHA-256. A missing or unknown token returns `401`.

## Errors

Errors return a JSON body with a `detail` message:

```json theme={"system"}
{ "detail": "missing bearer token" }
```

| Status | When |
| - | - |
| `400` | Invalid JSON, or a request with the wrong schema |
| `401` | Missing or invalid bearer token |
| `402` | Cloud verification quota exhausted |
| `403` | Not a member of the organisation |
| `404` | No such model, version, package, job or lemma |
| `413` | Request too large (64 MiB for `/v1/verify`, 8 MiB for deposits) |

## Typical flows

> [accordion] Resolve and download a spec (what `theformalera pull` does)
>
> 1. `GET /v1/specs/{org}/{model}`: list the versions and pick the newest that satisfies the requirement.
> 2. `GET /v1/specs/{org}/{model}/{version}/package`: download the archive (on AWS: a redirect to a pre-signed URL).
> 3. `GET /v1/keys`: verify the manifest's signature against the publisher keys.
> 4. `GET /v1/advisories`: warn if the locked version is affected.

> [accordion] Verify in the cloud (what `--runner cloud` does)
>
> 1. `POST /v1/verify` with a `theformalera.request/v1` body. The response is `202 { "job": "J-…", "status": "queued" }`.
> 2. `GET /v1/jobs/{job_id}` until `status` is `done` or `failed`. A `done` job includes the engine's response: results, certificates and lemma information.

> [accordion] Use and grow the Lemma Hub (what every verify does)
>
> 1. `POST /v1/lemmas/prefetch` with the run's Op Specs and Spec Keys, before solving.
> 2. `POST /v1/lemmas/deposit` with new lemmas and open goals, after solving. The response is `202 { "submission": "D-…" }`; admission happens later, on the Hub.
> 3. `POST /v1/lemmas/usage` with hit counts.

## Endpoints

The endpoint pages in this tab are generated from the API's OpenAPI document (`/api-reference/openapi.json`). Every request and response example on them was captured from a real local Hub.


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