Skip to main content
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
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:
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

Quickstart

Verify the example repository on your machine in about ten minutes.

Tutorial: onboard a repository

Annotate, pull, verify, fix a bug, gate CI and sign off a release.

How it works

From kernel source to a Lean 4 certificate: what is proved, and what is trusted.

Supported models

Lean 4 specs for eight models, from Qwen3-0.6B to Muse-Glimmer-30B.

​
What you get

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).
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.
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.
Reusable sub-proofs are stored as lemmas in the Lemma Hub. Later kernels, autotune configs and models cite them instead of searching again. Lemmas only change speed, never verdicts.
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.

​
The parts

​
Watch the demo

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.