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

# Run modes

> Solve on your own runner, in the cloud, or in your data center.

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

```toml theformalera.toml theme={"system"}
[verify]
runner = "local"
```

```bash theme={"system"}
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

```toml theformalera.toml theme={"system"}
[verify]
runner = "cloud"
```

```bash theme={"system"}
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

```toml theformalera.toml theme={"system"}
[verify]
runner = "on-prem"
```

```bash theme={"system"}
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](https://docs.theformalera.com/self-hosting/overview.md).

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


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