Skip to main content
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.
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.
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.
Install the engine (pip install "theformalera[engine]", from the licensed index), or use --runner cloud.
pull and local verification need lake. Install elan. The CLI also looks in ~/.elan/bin, so a shell without elan on its PATH still works.
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.
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.
Kernel annotations must give the grid, for example grid=("T", "cdiv(17408, BLOCK)"). Only launcher-level annotations may omit it.
domain= may only narrow the model’s default shape domain. Use bounds inside it.
Per-layer nodes need a layer selector, and top-level nodes (embed, final_norm, lm_head) must not have one. See Spec Keys.
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.
The engine reached a construct it cannot prove yet. This is common for attention, Gated DeltaNet and CUTLASS kernels; see Limitations. Read detail and stuck_at in the JSON report, then rewrite, waive, or wait for the nightly retry.
signoff needs a whole-project run, so that its coverage claims cover everything. Run theformalera verify with no paths and no --changed-only first.
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.
Your plan’s cloud quota is used up. Switch to --runner local or raise the quota.
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 with load_weights.
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.