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

# Installation

> Install the theformalera CLI, the Lean 4 toolchain and, for local solving, the verification engine.

## The CLI

```bash theme={"system"}
pip install theformalera
```

The package provides the `theformalera` command and the Python annotation SDK (`import theformalera as tfe`). It needs Python 3.10 or newer and runs on Linux and macOS.

| Extra | Install | Adds |
| - | - | - |
| `triton` | `pip install "theformalera[triton]"` | Triton, used to lower kernels to Triton IR. It runs on the CPU: no GPU is needed. |
| `engine` | `pip install "theformalera[engine]"` | The verification engine, for `runner = "local"`. Licensed; distributed from the private package index. |
| `mcp` | `pip install "theformalera[mcp]"` | The MCP server for coding agents (`theformalera mcp`). |

A CI runner that sends work to the cloud solver needs only `theformalera[triton]`. A runner that solves locally needs `theformalera[triton,engine]`.

> [!NOTE]
>
> Annotations are no-ops at runtime. Your inference code can import `theformalera` in production without pulling in Triton, Lean or the engine.

## Lean 4

`theformalera pull` builds each spec package as a Lean 4 (Lake) workspace, and `local` verification checks every proof with the Lean kernel. Install Lean with [elan](https://lean-lang.org/install/):

```bash theme={"system"}
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
```

The CLI looks for `lake` on your `PATH` and then in `~/.elan/bin`. The toolchain version comes from each spec package (`leanprover/lean4:v4.35.0` today), and elan installs it on first use.

> [!TIP]
>
> The first `pull` downloads Mathlib's prebuilt cache (several GB). Set `THEFORMALERA_MATHLIB` to an existing Lake workspace that already has Mathlib built, and every spec workspace reuses it instead.

You can skip Lean when you use `--runner cloud`: proofs are checked in the cloud, and `theformalera pull --no-build` skips the local build. You still need Lean to [re-check proofs](https://docs.theformalera.com/guides/recheck-proofs.md) yourself.

## Log in to Spec Hub

```bash theme={"system"}
theformalera login                  # opens the browser; paste the token shown after sign-in
theformalera login --token tfe_…    # or pass it directly
```

The token is stored in `~/.config/theformalera/credentials.json` (mode `0600`). In CI, set `THEFORMALERA_TOKEN` instead. Public specs and the public lemma library can be read without a token; cloud verification and the org lemma library need one.

## Check the install

```bash theme={"system"}
theformalera version
```

```text theme={"system"}
theformalera 0.9.0 · theformalera engine 2026.10
```

Without the `engine` extra, the second part reads `theformalera engine (remote)`.

## Developing The Formal Era itself

The source repository is a uv workspace with four packages, the Lean library and the AWS app:

```bash theme={"system"}
uv sync --extra cuda --extra nvcc --group dev      # or --extra cpu on machines without a GPU
(cd specs && lake exe cache get && lake build)     # Lean 4 spec library, proofs, oracle
uv run pytest                                      # CLI, engine, Hub, conformance, kernel evidence
(cd infra && uv sync --group dev && uv run --group dev pytest tests)   # CDK synthesis tests
```

| Package | Contents |
| - | - |
| `packages/theformalera` | The public CLI and annotation SDK |
| `packages/theformalera-engine` | The verification engine (proprietary) and the kernel-evidence stage |
| `packages/theformalera-hub` | Spec Hub and Lemma Hub: publisher, API, website, solve worker, admission |
| `packages/theformalera-conformance` | Conformance of PyTorch model implementations to the Model Specs |
| `specs/` | The Lean 4 library `TheFormalEra`: Op Specs, Model Specs, oracle, theorems, engine semantics |
| `infra/` | AWS CDK app for the hosted Hub |


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