Skip to main content
In this quickstart you run the whole loop on your own machine. You publish the Lean 4 specs to a local Spec Hub (a directory). Then you verify the Triton kernels of the example repository against them, and read the counterexample for the one kernel that is wrong. A CPU is enough.
The quickstart uses a local file:// Hub built from this repository, so it needs no account and no network access beyond the first Mathlib download. To use the hosted Spec Hub instead, see Installation.

​
Prerequisites

  • Linux or macOS with Python 3.12 and uv
  • elan (the Lean 4 toolchain manager); lake must be on your PATH, or in ~/.elan/bin
  • About 8 GB of free disk space for Mathlib’s build cache
1

Get the repository and its dependencies

2

Build the Lean 4 spec library

This compiles the Op Specs, the Model Specs of all eight models, the executable oracle, and every theorem. lake exe cache get downloads prebuilt Mathlib files instead of compiling Mathlib.
3

Publish the specs to a local Hub

Each model becomes a signed, content-addressed spec package in $WORK/hub.
4

Point the CLI at the local Hub

THEFORMALERA_HUB overrides the hub in theformalera.toml. THEFORMALERA_MATHLIB lets each spec workspace reuse the Mathlib build from step 2.
5

Pull and lock the specs

The lock records the version, content hash and Lean toolchain of every spec. Commit it, so CI and your laptop check against exactly the same specs.
6

Verify

Five kernels are proved for every shape in the model’s domain. The exit status is 1, because one kernel failed. That is what makes verify usable as a CI gate.
7

Read the counterexample

The kernel rounds the page count down, so the tokens of a partial last page are never read.

​
What just happened

  1. theformalera read the @tfe.implements(...) annotation on each kernel. Each annotation names a node of the Qwen3.8-27B compute graph, such as layers[*].input_norm.
  2. It lowered each kernel, once per autotune config, to Triton IR, on the CPU.
  3. The engine searched for counterexamples. Where there was none, it wrote a Lean 4 proof that the kernel equals the node’s Op Spec for every allowed shape, and the Lean kernel checked that proof.
  4. The proofs are in .theformalera/proofs/. They are ordinary Lean 4 files; see Re-check proofs.

​
Next steps

Fix it and finish the release

Continue with repro, the fix, waivers, CI and sign-off.

Annotate your own kernels

The @tfe.implements reference, with worked examples.