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

# Environment variables

> Variables read by the CLI, the engine, the Hub and the conformance verifier.

## CLI and engine

| Variable | Default | Meaning |
| - | - | - |
| `THEFORMALERA_TOKEN` | stored token | Spec Hub API token; takes precedence over `theformalera login` |
| `THEFORMALERA_HUB` | `[project] hub` | Hub URL; `file://<dir>` uses a local mirror |
| `THEFORMALERA_CACHE` | `~/.cache/theformalera` | Spec package cache (`specs/<digest>`) and compiled lemma packs |
| `THEFORMALERA_MATHLIB` | — | A Lake workspace with Mathlib built; spec workspaces reuse its `.lake/packages` |
| `THEFORMALERA_SPECS` | — | Use this Lean workspace for proof checks instead of the locked package's; also the spec library used by `theformalera-conformance` (default `specs/`) |
| `THEFORMALERA_ENGINE_URL` | — | The on-prem engine endpoint (`runner = "on-prem"`) |
| `THEFORMALERA_ORG` | `local-org` | Organisation name, for `file://` mirrors |
| `THEFORMALERA_PLAN` | `enterprise` | Plan reported by a `file://` mirror |
| `THEFORMALERA_SIGNING_KEY` | `.theformalera/signing-key.pem` | Release signing key for `signoff` |
| `THEFORMALERA_SIGNER_PUBKEY` | — | Public key for `cert verify` |
| `THEFORMALERA_GUARDS` | `1` | Set to `0` to disable the generated runtime guards |
| `THEFORMALERA_KEEP_CERTS` | — | Directory where the engine keeps every generated certificate, including rejected ones (debugging) |
| `XDG_CONFIG_HOME` | `~/.config` | Location of `theformalera/credentials.json` |

## Hub API

| Variable | Default | Meaning |
| - | - | - |
| `THEFORMALERA_HUB_STORE` | `hub-data` | Object store: a directory or `s3://bucket/prefix` |
| `THEFORMALERA_HUB_JOBS` | jobs in the store directory | DynamoDB table of jobs |
| `THEFORMALERA_HUB_TOKENS` | `tokens.json` in the store | DynamoDB table of API tokens |
| `THEFORMALERA_HUB_QUEUE` | in-store queue file | SQS queue URL for verification jobs |
| `THEFORMALERA_HUB_PUBLIC_URL` | — | Public URL, for redirects to the website |

## Conformance

| Variable | Default | Meaning |
| - | - | - |
| `THEFORMALERA_SPECS` | `specs/` of the repository | The Lean spec library and its `theformalera-spec` executable |
| `HF_HOME` / `HF_HUB_CACHE` | Hugging Face defaults | Where `config.json` files and checkpoints are cached |


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