# The Formal Era

> Formal verification of inference kernels, as a test in CI: Lean 4 specs of language models, machine-checked proofs of Triton kernels, and conformance checks of PyTorch model implementations.

- [The Formal Era](https://docs.theformalera.com/index.md): Formal verification of inference kernels, as a test in CI. Every PASS ships with a Lean 4 proof you can re-check yourself.
- [Quickstart](https://docs.theformalera.com/quickstart.md): Verify the example repository against a local Spec Hub and read your first counterexample.
- [Installation](https://docs.theformalera.com/installation.md): Install the theformalera CLI, the Lean 4 toolchain and, for local solving, the verification engine.
- [Tutorial: onboard a repository](https://docs.theformalera.com/tutorial.md): From an unannotated set of Triton kernels to a gated CI check and a signed release certificate.
- [How it works](https://docs.theformalera.com/concepts/how-it-works.md): What happens between `theformalera verify` and a verdict, and what a PASS actually proves.
- [Spec Keys](https://docs.theformalera.com/concepts/spec-keys.md): How an annotation names the part of a model's compute graph a kernel implements.
- [Op Specs and Model Specs](https://docs.theformalera.com/concepts/specs.md): What a Lean 4 spec says, what it leaves out, and how a model's compute graph is built from it.
- [Verdicts](https://docs.theformalera.com/concepts/verdicts.md): PASS, FAILED and UNKNOWN, their subtypes, and what CI does with each.
- [Lemma Hub](https://docs.theformalera.com/concepts/lemma-hub.md): How reusable sub-proofs are retrieved before solving and deposited after, and why they change speed but never verdicts.
- [Trust model](https://docs.theformalera.com/concepts/trust-model.md): What you have to trust for a PASS to mean what it says, and what you can check yourself.
- [Limitations](https://docs.theformalera.com/concepts/limitations.md): What is out of scope by design, and what the engine cannot prove yet.
- [Annotate Triton kernels](https://docs.theformalera.com/guides/annotate-triton.md): Declare which spec node a Triton kernel implements, how its parameters bind, and which configs to verify.
- [Annotate CUDA and CUTLASS kernels](https://docs.theformalera.com/guides/annotate-cuda.md): Comment or macro annotations for C++ kernels, template instances, and what the engine does with them today.
- [Layouts and assumptions](https://docs.theformalera.com/guides/layouts-and-assumptions.md): Tell the engine how physical storage maps to the spec's logical tensors, and which preconditions a kernel relies on.
- [Fix a failure](https://docs.theformalera.com/guides/fix-a-failure.md): Read a counterexample, reproduce it on the GPU, and confirm the fix.
- [Continuous integration](https://docs.theformalera.com/guides/ci.md): Make verification a required check on GitHub, GitLab or Buildkite, and run the quick level before every commit.
- [Policy and waivers](https://docs.theformalera.com/guides/policy-and-waivers.md): Decide which verdicts fail CI, and record time-limited exceptions with an owner.
- [Run modes](https://docs.theformalera.com/guides/run-modes.md): Solve on your own runner, in the cloud, or in your data center.
- [Release sign-off](https://docs.theformalera.com/guides/release-signoff.md): Coverage levels L1–L3, the signed release certificate, and the deployment gate.
- [Re-check proofs](https://docs.theformalera.com/guides/recheck-proofs.md): Check a release's proofs with stock Lean 4 and Mathlib, without any theformalera code.
- [Coding agents (MCP)](https://docs.theformalera.com/guides/coding-agents.md): Let the agent that writes your kernels read the spec and verify while it generates.
- [RL environment](https://docs.theformalera.com/guides/rl-environment.md): Use the verifier as the reward gate when training models to write kernels.
- [Write and check a spec](https://docs.theformalera.com/guides/write-a-spec.md): Draft a Model Spec from a torch.export graph, add a model to the Lean library, and check it.
- [Model conformance](https://docs.theformalera.com/conformance/overview.md): Check that a PyTorch implementation of a whole model computes exactly what its Lean 4 Model Spec says.
- [Verify your implementation](https://docs.theformalera.com/conformance/verify-an-implementation.md): Point the conformance verifier at a PyTorch file, and read where it disagrees with the spec.
- [Results for the official implementations](https://docs.theformalera.com/conformance/results.md): Measured conformance of the official Hugging Face implementation of every supported model to its Lean 4 spec.
- [The tail-page bug random tests miss](https://docs.theformalera.com/case-studies/boundary-bug.md): A paged decode attention kernel passes its differential tests and is wrong for 60 of 64 sequence lengths.
- [Reward hacking an allclose check](https://docs.theformalera.com/case-studies/reward-hacking.md): Three RMSNorm kernels from an RL policy pass the reward check; the spec gate rejects all three.
- [Races and overflows, without a GPU](https://docs.theformalera.com/case-studies/unsafe-without-gpu.md): Four kernels with schedule- and shape-dependent defects, caught on a machine with no visible GPU in 5.7 s.
- [The Lemma Hub flywheel, measured](https://docs.theformalera.com/case-studies/lemma-flywheel.md): Eleven sequential verifications on one machine: what the Lemma Hub changes, and what it does not.
- [Troubleshooting](https://docs.theformalera.com/troubleshooting.md): Common errors and what to do about them.
- [FAQ](https://docs.theformalera.com/faq.md): Short answers to common questions.
- [Supported models](https://docs.theformalera.com/models/index.md): The Lean 4 Model Specs on Spec Hub, their architectures and their conformance status.
- [Op Specs](https://docs.theformalera.com/models/op-specs.md): The operator definitions every Model Spec is built from, in Lean 4.
- [Qwen3-0.6B](https://docs.theformalera.com/models/qwen3-0-6b.md): Dense Qwen3: GQA attention with per-head q/k RMSNorm, SwiGLU, tied embeddings.
- [Qwen3.8-27B](https://docs.theformalera.com/models/qwen3-8-27b.md): Hybrid Qwen3.5-family model: 48 Gated DeltaNet layers and 16 gated attention layers.
- [gemma-4-12B](https://docs.theformalera.com/models/gemma-4-12b.md): Gemma 4: 5 sliding-window layers per global layer, sandwich norms, logit soft-capping.
- [gemma-4-31B](https://docs.theformalera.com/models/gemma-4-31b.md): Gemma 4: 5 sliding-window layers per global layer, sandwich norms, logit soft-capping.
- [granite-4.2-3b](https://docs.theformalera.com/models/granite-4-2-3b.md): Dense Granite: GQA attention with a µP-style attention multiplier, SwiGLU.
- [granite-4.2-8b](https://docs.theformalera.com/models/granite-4-2-8b.md): Dense Granite: GQA attention with a µP-style attention multiplier, SwiGLU.
- [granite-4.2-30b](https://docs.theformalera.com/models/granite-4-2-30b.md): Dense Granite: GQA attention with a µP-style attention multiplier, SwiGLU.
- [Muse-Glimmer-30B](https://docs.theformalera.com/models/muse-glimmer-30b.md): Muse Glimmer: 3 sliding-window layers per NoPE global layer, gated attention, sandwich norms.
- [CLI overview](https://docs.theformalera.com/reference/cli/overview.md): Every command of the three command-line tools, and their common behaviour.
- [Project commands](https://docs.theformalera.com/reference/cli/project.md): login, init, scan, pull, annotate and version.
- [Verification commands](https://docs.theformalera.com/reference/cli/verification.md): verify, explain, repro, guards and mcp.
- [Release commands](https://docs.theformalera.com/reference/cli/release.md): coverage, trace, signoff and cert verify.
- [Spec commands](https://docs.theformalera.com/reference/cli/specs.md): spec show, spec new and spec check.
- [Lemma commands](https://docs.theformalera.com/reference/cli/lemmas.md): lemma show, lemma search, lemma list and lemma preview.
- [theformalera-conformance](https://docs.theformalera.com/reference/cli/conformance.md): models, spec, prove, verify and verify-all.
- [theformalera-hub](https://docs.theformalera.com/reference/cli/hub.md): Operate a Spec Hub: keys, publishing, the API server, the solve worker, tokens, advisories and the Lemma Hub.
- [theformalera.toml](https://docs.theformalera.com/reference/configuration.md): Every section and key of the project configuration file.
- [Annotation reference](https://docs.theformalera.com/reference/annotations.md): The full syntax of @tfe.implements, tfe.layout, and the C++ comment and macro forms.
- [Python API](https://docs.theformalera.com/reference/python-api.md): The public Python interface of the theformalera package.
- [Environment variables](https://docs.theformalera.com/reference/environment-variables.md): Variables read by the CLI, the engine, the Hub and the conformance verifier.
- [Reports](https://docs.theformalera.com/reference/reports.md): The run report, the result record, SARIF, the PR comment and the HTML report.
- [Release certificate](https://docs.theformalera.com/reference/certificate.md): The signed in-toto statement that theformalera signoff produces and cert verify checks.
- [Spec packages](https://docs.theformalera.com/reference/spec-packages.md): What a published spec package contains, how it is versioned, signed and locked.
- [Spec Hub API](https://docs.theformalera.com/api-reference/introduction.md): The HTTP API behind theformalera: the spec registry, cloud verification and the Lemma Hub.
- [Health check](https://docs.theformalera.com/api-reference/registry/health-check.md): Liveness of the API.
- [List models](https://docs.theformalera.com/api-reference/registry/list-models.md): Every model key with a published Model Spec, with its latest version.
- [List versions of a spec](https://docs.theformalera.com/api-reference/registry/list-versions-of-a-spec.md): Published versions of a model's spec package, and the security advisories that affect it.
- [Get a spec manifest](https://docs.theformalera.com/api-reference/registry/get-a-spec-manifest.md): The manifest of one package version: compute-graph nodes (Op Spec, formula, constants, tensors), value flow, default shape and value domains, the Hugging Face config the spec renders, the audited theorems, trust status and the publisher signature. `version` is the full version (`1.0.0`).
- [Download a spec package](https://docs.theformalera.com/api-reference/registry/download-a-spec-package.md): The package archive (`.tgz`: Lean sources + manifest). On AWS the API answers with a 302 redirect to a pre-signed S3 URL. Packages are immutable and cached for a year.
- [List advisories](https://docs.theformalera.com/api-reference/registry/list-advisories.md): Spec security advisories. `theformalera pull` warns when the lock pins an affected version.
- [List publisher keys](https://docs.theformalera.com/api-reference/registry/list-publisher-keys.md): Public keys that sign spec packages. The CLI verifies every downloaded package against them.
- [Who am I](https://docs.theformalera.com/api-reference/verification/who-am-i.md): The tenant and plan of the token.
- [Submit a verification](https://docs.theformalera.com/api-reference/verification/submit-a-verification.md): Queue a verification request (`theformalera.request/v1`) for the cloud solve workers. The request carries the lowered Triton IR of every constexpr configuration, the annotations and the resolved spec nodes; never the repository. Poll the returned job with `GET /v1/jobs/{job_id}`. Requests are limite…
- [Get a job](https://docs.theformalera.com/api-reference/verification/get-a-job.md): Status of a verification job; once `done`, the engine response is included.
- [Look up cached results](https://docs.theformalera.com/api-reference/verification/look-up-cached-results.md): Cached results by cache key (lowered-IR hash + spec hash + engine version + assumptions). At most 500 keys per call; misses are omitted.
- [Prefetch lemmas](https://docs.theformalera.com/api-reference/lemma-hub/prefetch-lemmas.md): Lemmas for the Op Specs of a verification, plus the general ones, from the requested libraries. Only op names and Spec Keys are sent. Without a token only the public library is searched. Results are capped (default 256, max 512) and ranked by hit count; lemmas pending migration are skipped.
- [Search lemmas](https://docs.theformalera.com/api-reference/lemma-hub/search-lemmas.md): Search the public library (and the caller's org library with a token) by statement text, Op Spec or node. At most 200 results.
- [Get a lemma](https://docs.theformalera.com/api-reference/lemma-hub/get-a-lemma.md): One lemma record. Public lemmas never show the contributing organisation.
- [Deposit lemmas](https://docs.theformalera.com/api-reference/lemma-hub/deposit-lemmas.md): Queue new lemmas and open goals for admission. Nothing is trusted as submitted: the admission task regenerates every lemma from the template, compiles it with Lean against the Hub's spec package, enforces the axiom allowlist and re-derives the visibility. At most 500 lemmas and 500 open goals, 8 MiB…
- [Report lemma usage](https://docs.theformalera.com/api-reference/lemma-hub/report-lemma-usage.md): Hit counts of a run (lemma ids, counts, project). Never code. Feeds the hit statistics and the website's node pages.
- [Get the contribution cap](https://docs.theformalera.com/api-reference/lemma-hub/get-the-contribution-cap.md): The organisation's contribution cap. A repository's `[lemmas] contribute` can only be stricter.
- [Self-hosting overview](https://docs.theformalera.com/self-hosting/overview.md): Run your own Spec Hub: a directory mirror, a local API server, or the AWS deployment.
- [Local Hub](https://docs.theformalera.com/self-hosting/local-hub.md): A Spec Hub in a directory, for development, offline CI and air-gapped mirrors.
- [Publish specs](https://docs.theformalera.com/self-hosting/publish-specs.md): Build, audit, sign and publish spec packages to a Hub store.
- [Deploy on AWS](https://docs.theformalera.com/self-hosting/aws.md): The CDK app that runs Spec Hub: storage, the API and website, and the solve workers.
- [Lemma administration](https://docs.theformalera.com/self-hosting/lemma-administration.md): Admission, contribution caps, audit logs, snapshots, migration and statistics of a Hub's Lemma Hub.

## OpenAPI Specs

- [openapi](/api-reference/openapi.json)


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