Installation

The CLI

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

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:

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.

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

Log in to Spec Hub

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

theformalera version

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:

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

Get started

Concepts

Guides

Model conformance

Case studies

Help

The CLI

Lean 4

Log in to Spec Hub

Check the install

Developing The Formal Era itself

​The CLI

​Lean 4

​Log in to Spec Hub

​Check the install

​Developing The Formal Era itself

The CLI

Lean 4

Log in to Spec Hub

Check the install

Developing The Formal Era itself