> ## 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. # Quickstart > Verify the example repository against a local Spec Hub and read your first counterexample. 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. > [!NOTE] > > 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](https://docs.theformalera.com/installation.md). ## Prerequisites * Linux or macOS with Python 3.12 and [uv](https://docs.astral.sh/uv/) * [elan](https://lean-lang.org/install/) (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** ```bash theme={"system"} git clone theformalera && cd theformalera uv sync --extra cpu --group dev # use --extra cuda on a GPU machine ``` **2. Build the Lean 4 spec library** ```bash theme={"system"} (cd specs && lake exe cache get && lake build) ``` 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** ```bash theme={"system"} export WORK=/tmp/tfe-quickstart REPO=$PWD uv run theformalera-hub keygen -o $WORK/publisher.pem uv run theformalera-hub publish --specs specs --store $WORK/hub \ --version 1.0.0 --key $WORK/publisher.pem --skip-build ``` ```text theme={"system"} published Qwen/Qwen3-0.6B@1.0.0 sha256:96fd971256defe9045d11d0cfeb33f0b32ff47419d8123b0b2c172c42dac5ac1 published Qwen/Qwen3.8-27B@1.0.0 sha256:313a42af237f0db7ec729fd0d5d9230d932d829da0cbda0c43bdb4d310aaddf4 published google/gemma-4-12B@1.0.0 sha256:6204c6466455d92cd9e4cf550f8179e48f10045a5dc436f6fd5d86608582418b … ``` Each model becomes a signed, content-addressed spec package in `$WORK/hub`. **4. Point the CLI at the local Hub** ```bash theme={"system"} cp -r examples/acme-qwen3.8-27b-h100 $WORK/acme && cd $WORK/acme rm -f theformalera.lock # the committed lock pins a different dev-Hub digest export THEFORMALERA_HUB=file://$WORK/hub THEFORMALERA_MATHLIB=$REPO/specs ``` `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** ```bash theme={"system"} uv run --project $REPO theformalera pull ``` ```text theme={"system"} ✓ Qwen/Qwen3.8-27B@1.0.0 sha256:313a42af237f… signed theformalera (verified) wrote theformalera.lock (1 spec) ``` 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** ```bash theme={"system"} uv run --project $REPO theformalera verify ``` ```text theme={"system"} theformalera 0.9.0 · specs locked by theformalera.lock kernel spec node configs result level / id time ─────────────────────────────────────────────────────────────────────────────────────────── silu_mul_kernel layers[*].mlp.act 1/1 PASS PROVED 3.4s silu_mul_tanh_kernel layers[*].mlp.act 4/4 PASS PROVED 15.2s paged_decode_attention layers[*].attn.core 0/1 FAILED F-0001 1.8s rmsnorm_kernel layers[*].input_norm 1/1 PASS PROVED 3.4s rmsnorm_kernel layers[*].post_attn_norm 1/1 PASS PROVED 3.5s residual_add_kernel layers[*].attn_residual 1/1 PASS PROVED 3.0s 5 passed · 1 failed · 0 unknown run `theformalera explain F-0001` lemma hub: 14 hits (14 built-in) · 1 new → local-org ``` 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** ```bash theme={"system"} uv run --project $REPO theformalera explain F-0001 ``` ```text theme={"system"} 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 notes swept seq_len = 1..64: 4 correct, 60 wrong suspect kernels/attn_decode.py:39 n_pages = seq_len // PAGE_SIZE # expected: tl.cdiv(seq_len, PAGE_SIZE) ``` 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](https://docs.theformalera.com/guides/recheck-proofs.md). ## Next steps > [card] [Fix it and finish the release](https://docs.theformalera.com/tutorial.md) > > Continue with repro, the fix, waivers, CI and sign-off. > [card] [Annotate your own kernels](https://docs.theformalera.com/guides/annotate-triton.md) > > The `@tfe.implements` reference, with worked examples. This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.