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

# theformalera.toml

> Every section and key of the project configuration file.

`theformalera.toml` lives at the root of your repository; `theformalera init` writes it. Commit it, together with `theformalera.lock`.

```toml theformalera.toml theme={"system"}
[project]
name = "acme-qwen3.8-27b-h100"
hub  = "https://hub.theformalera.com"

[scan]
include = ["kernels/**/*.py", "csrc/**/*.cu", "csrc/**/*.cuh"]
exclude = ["**/tests/**", "**/benchmarks/**"]

[targets]
triton  = { arch = ["sm_90a"] }
cutlass = { arch = ["sm_90a"], include = ["third_party/cutlass/include"] }

[models]
"Qwen/Qwen3.8-27B" = { version = "^1.0" }

[verify]
level = "proof"              # proof | bounded | quick
timeout_per_kernel = "15m"
runner = "local"             # local | cloud | on-prem

[policy]
require_level      = "proof"
allow_bounded_on   = ["kernels/experimental/**"]
fail_on            = ["counterexample", "unsafe", "overflow", "vacuous", "unknown"]
require_annotation = ["kernels/**/*.py", "csrc/**/*.cu"]
domain_narrowing   = "warn"

[[waiver]]
id      = "W-12"
kernel  = "GateUpGemm<64x128x64,WS>"
verdict = "unknown"
reason  = "warp-specialized pipeline not yet supported; covered by differential tests"
owner   = "alice"
expires = 2026-11-30

[trusted]
nodes = ["lm_head", "embed"]   # nodes computed by trusted external libraries (cuBLAS, ...)

[lemmas]
use        = ["public", "org"]   # which Lemma Hub libraries to search
contribute = "org"               # off | org | public: where lemmas from this project go
snapshot   = "latest"            # or a snapshot time, to reproduce the solving process bit for bit
```

## `[project]`

**name** `string` (default: the directory name)

Project name. It appears in reports, in cloud requests and as the certificate's subject.

**hub** `string` (default: [https://hub.theformalera.com](https://hub.theformalera.com))

Spec Hub URL. `THEFORMALERA_HUB` overrides it; `file://<dir>` uses a local mirror.

## `[scan]`

**include** `list[glob]` (default: \["**/\*.py", "**/*.cu", "\*\*/*.cuh"])

Files to scan for annotations.

**exclude** `list[glob]` (default: \["**/tests/**", "**/benchmarks/**", ".venv/\*\*"])

Files to skip.

## `[targets]`

**triton.arch** `list[str]` (default: \["sm\_90a"])

Target architecture for lowering. The first entry is used for lowering and recorded as the certificate's hardware.

**cutlass.arch** `list[str]`

Target architectures of CUTLASS instances.

**cutlass.include** `list[str]`

CUTLASS include directories.

## `[models]`

One entry per model you deploy: `"<org>/<model>" = { version = "<requirement>" }`. The short form `"<org>/<model>" = "^1.0"` works too. Requirements use semver ranges: `^1.0`, `~1.0.2`, `>=1.0.2`, `1.0` (prefix match: any `1.0.x`), `*`; separate several with commas. `theformalera pull` resolves them and pins the result in the lock.

## `[verify]`

**level** `"proof" | "bounded" | "quick"` (default: proof)

Default verification level; see [Verdicts](https://docs.theformalera.com/concepts/verdicts.md#levels).

**timeout\_per\_kernel** `duration` (default: 15m)

Time budget per kernel, as `90s`, `15m`, `1h` or a number of seconds.

**runner** `"local" | "cloud" | "on-prem"` (default: local)

Where the engine runs; see [Run modes](https://docs.theformalera.com/guides/run-modes.md).

## `[policy]`

See [Policy and waivers](https://docs.theformalera.com/guides/policy-and-waivers.md).

**require\_level** `"proof" | "bounded"` (default: proof)

With `proof`, BOUNDED fails outside `allow_bounded_on`.

**allow\_bounded\_on** `list[glob]` (default: \[])

Files where BOUNDED passes even under `require_level = "proof"`.

**fail\_on** `list[str]` (default: \["counterexample", "unsafe", "overflow", "vacuous", "unknown"])

Verdict kinds that fail the run.

**require\_annotation** `list[glob]` (default: \[])

Every `@triton.jit` kernel under these paths must be annotated.

**domain\_narrowing** `"allow" | "warn" | "fail"` (default: warn)

Accepted, reserved for policing `domain=` narrowing; not enforced in this release.

## `[[waiver]]`

One table per waiver. `id`, `kernel` (an fnmatch pattern on the kernel name), `verdict` (a verdict or kind), `reason`, `owner` and `expires` (a date) are required. `approved_by` is required to waive COUNTEREXAMPLE or UNSAFE.

## `[trusted]`

**nodes** `list[str]` (default: \[])

Graph nodes computed by external libraries, counted as covered for L2 and listed in the certificate's `trusted` field.

## `[lemmas]`

See [Lemma Hub](https://docs.theformalera.com/concepts/lemma-hub.md#where-lemmas-go).

**use** `list["public" | "org"]` (default: \["public", "org"])

Libraries to retrieve lemmas from.

**contribute** `"off" | "org" | "public"` (default: depends on plan and runner)

Where lemmas from this project go. Without the key: `public` on the free tier in cloud mode, `org` on Team/Enterprise in cloud mode and in on-prem mode, `off` in local mode. Never looser than the organisation's cap.

**snapshot** `string` (default: latest)

`latest`, or a snapshot time. Lemmas created after it are not retrieved, which reproduces a solving process exactly.

## theformalera.lock

Written by `theformalera pull`; do not edit it by hand.

```toml theformalera.lock theme={"system"}
# generated by `theformalera pull`: commit this file so CI and local runs verify
# against exactly the same specs
[[spec]]
key = "Qwen/Qwen3.8-27B"
version = "1.0.0"
digest = "sha256:313a42af237f0db7ec729fd0d5d9230d932d829da0cbda0c43bdb4d310aaddf4"
lean_toolchain = "leanprover/lean4:v4.35.0"
publisher = "theformalera (verified)"
```


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