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

# The Formal Era

> Formal verification of inference kernels, as a test in CI. Every PASS ships with a Lean 4 proof you can re-check yourself.

The Formal Era checks that a GPU kernel computes exactly what one layer of a model is supposed to compute. You mark each Triton kernel with the model node it implements. `theformalera verify` fetches that node's Lean 4 specification from Spec Hub and returns a verdict. No GPU is needed.

![theformalera verify output: five kernels PASS with PROVED, paged\_decode\_attention FAILED with F-0001, and the Lemma Hub summary line](https://mintcdn.com/n-a-24de7f09/RKvaTncjzKh3Uq1K/images/screenshots/screenshot4-verified-operator-table.png?fit=max\&auto=format\&n=RKvaTncjzKh3Uq1K\&q=85\&s=622df6602859f729dd6a02b051ae4019)

Every **PASS** comes with a Lean 4 proof. The standard Lean 4 toolchain can re-check it, so you don't have to trust our engine, or us. Every **FAILED** comes with a concrete input that breaks the kernel, the shapes on which it is still correct, and the line to look at:

```text theme={"system"}
$ theformalera explain F-0001
F-0001  COUNTEREXAMPLE  paged_decode_attention -> Qwen/Qwen3.8-27B@1.0:layers[*].attn.core
failing configs    1 of 1
witness (minimal)  B=1, seq_len=1           o[0, 0, 0]: kernel nan, spec -0.253953
witness (typical)  B=1, seq_len=17          o[0, 0, 0]: kernel -0.163625, spec -0.17983
correct only when  seq_len % 16 == 0

  suspect  kernels/attn_decode.py:39
           n_pages = seq_len // PAGE_SIZE      # expected: tl.cdiv(seq_len, PAGE_SIZE)
```

A differential test with the usual sequence lengths (128, 512, 1024, 2048) passes this kernel. The tokens of the last, partial page are never read, so it is wrong for 60 of the 64 sequence lengths from 1 to 64.

## Start here

> [card] [Quickstart](https://docs.theformalera.com/quickstart.md)
>
> Verify the example repository on your machine in about ten minutes.

> [card] [Tutorial: onboard a repository](https://docs.theformalera.com/tutorial.md)
>
> Annotate, pull, verify, fix a bug, gate CI and sign off a release.

> [card] [How it works](https://docs.theformalera.com/concepts/how-it-works.md)
>
> From kernel source to a Lean 4 certificate: what is proved, and what is trusted.

> [card] [Supported models](https://docs.theformalera.com/models/index.md)
>
> Lean 4 specs for eight models, from Qwen3-0.6B to Muse-Glimmer-30B.

## What you get

> [accordion] A correctness test in CI, not a research project
>
> You write annotations and read reports. You never write Lean. Verification runs as a required check next to your unit tests. The GitHub Action posts a PR comment and line annotations (SARIF).

> [accordion] Proofs over every shape, not samples
>
> A PROVED kernel is correct for **every** shape in the model's domain (for example, every `T` from 1 to 262,144), not just the shapes a test happened to try. Every `@triton.autotune` config is verified, because any of them can be picked at runtime.

> [accordion] Honest verdicts
>
> When the engine cannot decide, the result is UNKNOWN, never PASS. Bugs in safety and numerics are reported too: out-of-bounds accesses, data races, integer overflow and float overflow.

> [accordion] Verification that gets faster with use
>
> Reusable sub-proofs are stored as lemmas in the [Lemma Hub](https://docs.theformalera.com/concepts/lemma-hub.md). Later kernels, autotune configs and models cite them instead of searching again. Lemmas only change speed, never verdicts.

> [accordion] Specs you can trust
>
> Each model's Lean 4 spec is checked against the official Hugging Face implementation, layer by layer, in float64. The same check works on your own [PyTorch implementation](https://docs.theformalera.com/conformance/overview.md).

## The parts

| Part | What it is | How you use it |
| - | - | - |
| `theformalera` CLI and SDK | `pip install theformalera` | `init`, `scan`, `pull`, `verify`, `explain`, `repro`, `signoff`, … and `@tfe.implements` in your code |
| Spec Hub | A registry of Lean 4 specs: one Model Spec per model, built from shared Op Specs | `theformalera pull`, `theformalera spec show` |
| Lemma Hub | A registry of machine-checked lemmas that speed up later proofs | Works in the background; `theformalera lemma show` and `lemma preview` |
| Verification engine | Lowers Triton to TTIR, searches for counterexamples, writes and checks Lean 4 proofs | Runs on your CI runner (`local`), in our cloud (`cloud`), or in your data center (`on-prem`) |
| CI plugins | GitHub Action, GitLab template, Buildkite step, pre-commit hooks | One `uses:` line, made a required check |
| `theformalera-conformance` | Checks a PyTorch model implementation against a Model Spec | `theformalera-conformance verify <model> <impl.py>` |

## Watch the demo

<video controls src="https://mintcdn.com/n-a-24de7f09/RKvaTncjzKh3Uq1K/videos/theformalera-demo.mp4?fit=max&auto=format&n=RKvaTncjzKh3Uq1K&q=85&s=5df16093694189126f85659435ee4dca" alt="Terminal recording of a theformalera session: scan, pull, verify, explain, repro, fix, waiver, lemma admission, proof re-check, guards, sign-off and the deployment gate" aria-label="Demo of the theformalera CLI">
  Your browser does not play embedded video. Download the demo from /videos/theformalera-demo.mp4.
</video>

A 3.7-minute session recorded from real runs against a local Hub. It shows scan, pull, verify, the Lemma Hub preview, explain, repro, the fix, a waiver, the Hub's Lean re-check of a deposited lemma, a lemma hit, re-checking a proof with stock Lean, runtime guards, sign-off and the deployment gate.


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