theformalera.toml lives at the root of your repository; theformalera init writes it. Commit it, together with theformalera.lock.
theformalera.toml
[project]
string
default:"the directory name"
Project name. It appears in reports, in cloud requests and as the certificate’s subject.
string
default:"https://hub.theformalera.com"
Spec Hub URL.
THEFORMALERA_HUB overrides it; file://<dir> uses a local mirror.[scan]
list[glob]
default:"[\"**/*.py\", \"**/*.cu\", \"**/*.cuh\"]"
Files to scan for annotations.
list[glob]
Files to skip.
[targets]
list[str]
default:"[\"sm_90a\"]"
Target architecture for lowering. The first entry is used for lowering and recorded as the certificate’s hardware.
list[str]
Target architectures of CUTLASS instances.
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]
duration
default:"15m"
Time budget per kernel, as
90s, 15m, 1h or a number of seconds.[policy]
See Policy and waivers.
"proof" | "bounded"
default:"proof"
With
proof, BOUNDED fails outside allow_bounded_on.list[glob]
default:"[]"
Files where BOUNDED passes even under
require_level = "proof".list[str]
Verdict kinds that fail the run.
list[glob]
default:"[]"
Every
@triton.jit kernel under these paths must be annotated."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]
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.
list["public" | "org"]
default:"[\"public\", \"org\"]"
Libraries to retrieve lemmas from.
"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.string
default:"latest"
latest, or a snapshot time. Lemmas created after it are not retrieved, which reproduces a solving process exactly.theformalera.lock
Written bytheformalera pull; do not edit it by hand.
theformalera.lock