Run modes

The engine is the same everywhere; only where it runs changes. Choose with [verify] runner or --runner.

Mode	Who solves	What leaves your machine	Lemma libraries	Best for
`local`	The engine on your runner (`theformalera[engine]`)	Nothing; specs and lemmas are pulled	Retrieves by spec node; new lemmas stay in the CI cache by default	Strict confidentiality and enough runner CPU
`cloud`	The solve workers behind Spec Hub	The lowered IR and annotations, never the repository	Public and org; deposits per `contribute`	Most teams; fastest PR feedback
`on-prem`	The enterprise engine in your data center	Nothing leaves your network	Your in-house org library plus a public mirror	Unreleased models

local

theformalera.toml

[verify]
runner = "local"

pip install "theformalera[triton,engine]"
theformalera pull            # also builds the Lean workspace: proofs are checked locally
theformalera verify

The engine needs Lean 4 (lake) and the built spec workspace. Results are cached in .theformalera/cache. Cache that directory, .theformalera/lemmas/local and ~/.cache/theformalera between CI runs; the GitHub Action does this for you.

cloud

theformalera.toml

[verify]
runner = "cloud"

export THEFORMALERA_TOKEN=tfe_…
theformalera pull --no-build     # the cloud checks the proofs; no local Lean build needed
theformalera verify

The CLI lowers each kernel locally and uploads a request (theformalera.request/v1) with the TTIR of every configuration, the annotations and the resolved spec nodes. It then polls the job and writes the returned certificates to .theformalera/proofs. Requests are limited to 64 MiB. Cloud verification counts against your plan’s quota; when the quota is exhausted, the run fails with cloud verification quota exhausted for this billing period.

on-prem

theformalera.toml

[verify]
runner = "on-prem"

export THEFORMALERA_ENGINE_URL=https://verify.internal.example.com
export THEFORMALERA_TOKEN=…
theformalera verify

The CLI posts the same request to $THEFORMALERA_ENGINE_URL/v1/solve and waits for the response. To also keep specs and lemmas in-house, run a self-hosted Hub; see Self-hosting.

Timeouts

[verify] timeout_per_kernel (default 15m; accepts 90s, 15m, 1h) bounds the Lean check of each kernel locally. In cloud and on-prem mode, the whole run may take timeout_per_kernel × number of kernels. A proof check that exceeds its budget is UNKNOWN · TIMEOUT.

Get started

Concepts

Guides

Model conformance

Case studies

Help

local

cloud

on-prem

Timeouts

​local

​cloud

​on-prem

​Timeouts

local

cloud

on-prem

Timeouts