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

# Troubleshooting

> Common errors and what to do about them.

> [accordion] no theformalera.toml found (run `theformalera init`)
>
> Project commands look for `theformalera.toml` in the current directory and its parents. Run them inside the project, or create the file with `theformalera init`.

> [accordion] Qwen/Qwen3.8-27B\@1.0.4 is not in the spec cache: run `theformalera pull`
>
> The lock pins a version that is not installed on this machine. Run `theformalera pull`. If the Hub cannot serve that version either (`not found in the mirror: …/1.0.4/package`), the lock was written against a different Hub. Run `theformalera pull --update` to re-resolve it.

> [accordion] downloaded package digest … does not match … (the lock pins a different package; refusing to continue)
>
> The Hub served different content for the locked version. On a public Hub this should never happen, since published versions are immutable, so treat it as a security event. On a dev Hub that was re-published, run `theformalera pull --update` deliberately and review the lock diff.

> [accordion] runner `local` needs the verification engine
>
> Install the engine (`pip install "theformalera[engine]"`, from the licensed index), or use `--runner cloud`.

> [accordion] Lean 4 not found: install elan to check proofs locally
>
> `pull` and local verification need `lake`. Install [elan](https://lean-lang.org/install/). The CLI also looks in `~/.elan/bin`, so a shell without elan on its `PATH` still works.

> [accordion] The first pull is slow or fills the disk
>
> The first build of a spec workspace downloads Mathlib's cache (several GB). Point `THEFORMALERA_MATHLIB` at a workspace with Mathlib already built, so every package reuses it. In CI with `runner = "cloud"`, use `pull --no-build`.

> [accordion] cannot bind spec tensor `x` to a kernel parameter
>
> The engine could not match the node's tensor `x` to a kernel argument by name. Add it to `bind=`, for example `bind={"X_ptr": "x"}`. `theformalera spec show <key>` lists the node's tensor names.

> [accordion] no launch grid (kernel-level annotations need `grid=`)
>
> Kernel annotations must give the grid, for example `grid=("T", "cdiv(17408, BLOCK)")`. Only launcher-level annotations may omit it.

> [accordion] domain: T ∈ \[1, 300000] widens the default domain \[1, 262144]
>
> `domain=` may only narrow the model's default shape domain. Use bounds inside it.

> [accordion] `attn.core` is a per-layer node: write `layers[*].attn.core`
>
> Per-layer nodes need a layer selector, and top-level nodes (`embed`, `final_norm`, `lm_head`) must not have one. See [Spec Keys](https://docs.theformalera.com/concepts/spec-keys.md).

> [accordion] annotation asks for …@1.1 but the lock pins 1.0.4
>
> The version in the annotation's Spec Key must match the lock. Drop the version from the key, or update `[models]` and run `theformalera pull --update`.

> [accordion] The result is UNKNOWN · unsupported
>
> The engine reached a construct it cannot prove yet. This is common for attention, Gated DeltaNet and CUTLASS kernels; see [Limitations](https://docs.theformalera.com/concepts/limitations.md). Read `detail` and `stuck_at` in the JSON report, then rewrite, waive, or wait for the nightly retry.

> [accordion] the last verification covered only kernels/x.py; run `theformalera verify` on the whole project before signing off
>
> `signoff` needs a whole-project run, so that its coverage claims cover everything. Run `theformalera verify` with no paths and no `--changed-only` first.

> [accordion] sign-off needs your confirmation to ship private lemmas (re-run with --yes)
>
> The proofs depend on lemmas from your organisation's private library. They must ship with the release so that customers can re-check it. Confirm with `--yes` if that is acceptable.

> [accordion] cloud verification quota exhausted for this billing period
>
> Your plan's cloud quota is used up. Switch to `--runner local` or raise the quota.

> [accordion] Conformance: cannot locate the decoder
>
> The verifier looks for a submodule with `embed_tokens` and `layers` at `model.language_model`, `model`, `language_model`, `transformer`, `decoder` or the root. Rename your modules to match, or use the [adapter style](https://docs.theformalera.com/conformance/verify-an-implementation.md) with `load_weights`.

> [accordion] Conformance passes at 1e-6 but fails at the default rtol
>
> A float32 computation is not being promoted to float64. Look for dtypes the verifier cannot intercept, such as custom ops, `half()`, or dtype arguments built from strings. Agreement for a correct implementation is around `1e-15`. If the difference is real, it is a real bug: an ε in the wrong place, for example, shows up at `1e-6`.


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