theformalera CLI is the main client of this API. You need it directly only to build your own tooling, a dashboard, or a mirror.
All endpoints are under
/v1 and exchange JSON, except the package download.
Authentication
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 adetail message:
Typical flows
Resolve and download a spec (what theformalera pull does)
Resolve and download a spec (what theformalera pull does)
GET /v1/specs/{org}/{model}: list the versions and pick the newest that satisfies the requirement.GET /v1/specs/{org}/{model}/{version}/package: download the archive (on AWS: a redirect to a pre-signed URL).GET /v1/keys: verify the manifest’s signature against the publisher keys.GET /v1/advisories: warn if the locked version is affected.
Verify in the cloud (what --runner cloud does)
Verify in the cloud (what --runner cloud does)
POST /v1/verifywith atheformalera.request/v1body. The response is202 { "job": "J-…", "status": "queued" }.GET /v1/jobs/{job_id}untilstatusisdoneorfailed. Adonejob includes the engine’s response: results, certificates and lemma information.
Use and grow the Lemma Hub (what every verify does)
Use and grow the Lemma Hub (what every verify does)
POST /v1/lemmas/prefetchwith the run’s Op Specs and Spec Keys, before solving.POST /v1/lemmas/depositwith new lemmas and open goals, after solving. The response is202 { "submission": "D-…" }; admission happens later, on the Hub.POST /v1/lemmas/usagewith 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.