Tutorial: onboard a repository

This tutorial follows one repository from start to finish. A coding agent has written Triton kernels for the text path of Qwen/Qwen3.8-27B on H100. You will annotate them, lock the specs, verify, fix the bug the verifier finds, waive what it cannot decide yet, wire it into CI, and sign off a release. All output on this page comes from real runs of examples/acme-qwen3.8-27b-h100. The Quickstart shows how to set up the local Hub these commands use.

Initialise the project

Run init at the repository root. It finds Triton and CUDA code and writes theformalera.toml:

theformalera init --model Qwen/Qwen3.8-27B

✓ wrote AGENTS.md (verification rules for coding agents)
✓ wrote theformalera.toml
  Triton code in: kernels   CUDA/CUTLASS code in: —
  Lemma Hub: lemmas from this project's proofs go to nowhere (local mode: they stay in this repository's CI
cache) (contribute = "off"; preview with `theformalera lemma preview`)

The generated file lists what to scan, which models you deploy, the verification level and the CI policy:

theformalera.toml

[project]
name = "acme-qwen3.8-27b-h100"
hub  = "https://hub.theformalera.com"

[scan]
include = ["kernels/**/*.py"]
exclude = ["**/tests/**", "**/benchmarks/**"]

[targets]
triton  = { arch = ["sm_90a"] }

[models]
"Qwen/Qwen3.8-27B" = { version = "^1.0" }

[verify]
level = "proof"              # proof | bounded | quick
timeout_per_kernel = "15m"
runner = "local"             # local | cloud | on-prem

[policy]
require_level      = "proof"
fail_on            = ["counterexample", "unsafe", "overflow", "vacuous", "unknown"]
require_annotation = ["kernels/**/*.py"]
domain_narrowing   = "warn"

[lemmas]
use        = ["public", "org"]   # which Lemma Hub libraries to search
contribute = "off"              # off | org | public: where lemmas from this project go
snapshot   = "latest"            # pin a snapshot to reproduce the solving process bit for bit

It also adds .theformalera/ to .gitignore and writes an AGENTS.md with the verification rules for coding agents.

Pull and lock the specs

theformalera pull

✓ Qwen/Qwen3.8-27B@1.0.0  sha256:313a42af237f…  signed theformalera (verified)
wrote theformalera.lock (1 spec)

theformalera.lock

# generated by `theformalera pull`: commit this file so CI and local runs verify
# against exactly the same specs
[[spec]]
key = "Qwen/Qwen3.8-27B"
version = "1.0.0"
digest = "sha256:313a42af237f0db7ec729fd0d5d9230d932d829da0cbda0c43bdb4d310aaddf4"
lean_toolchain = "leanprover/lean4:v4.35.0"
publisher = "theformalera (verified)"

pull checks the package’s signature and content hash, then builds its Lean workspace. Commit theformalera.lock.

Read the spec of the node you implement

theformalera spec show 'Qwen/Qwen3.8-27B@1.0:layers[*].input_norm'

input_norm   TheFormalEra.Ops.rmsnormOffset  ·  64 layer(s)
├── y[t,i] = x[t,i] / √(Σⱼ x[t,j]² / H + ε) · (1 + w[i])
├── constants: H=5120, eps=1e-06
├── tensors
│   ├── x        in      [T, 5120]  bf16
│   ├── w        weight  [5120]  bf16
│   ├── y        out     [T, 5120]  bf16
│   └── eps      scalar  []  f32
└── shape domain: T ∈ [1, 262144]

Note the (1 + w[i]). Qwen3.8 applies the RMSNorm weight as an offset. A kernel that multiplies by w, as most RMSNorm kernels do, is a counterexample for every T.

Annotate each kernel

Put @tfe.implements on every @triton.jit kernel. Here one kernel serves two nodes, so it lists two Spec Keys and is verified against each:

kernels/norm.py

import triton
import triton.language as tl

import theformalera as tfe


@tfe.implements(
    ["Qwen/Qwen3.8-27B@1.0:layers[*].input_norm",
     "Qwen/Qwen3.8-27B@1.0:layers[*].post_attn_norm"],   # the same kernel is used in two places
    grid=("T",),                                         # one program per row
    bind={"X": "x", "W": "w", "Y": "y", "eps": "eps"},
)
@triton.jit
def rmsnorm_kernel(X, W, Y, stride_x, stride_y, eps,
                   H: tl.constexpr, BLOCK: tl.constexpr):
    row = tl.program_id(0)
    cols = tl.arange(0, BLOCK)
    mask = cols < H
    x = tl.load(X + row * stride_x + cols, mask=mask, other=0.0).to(tl.float32)
    ms = tl.sum(x * x, axis=0) / H
    w = tl.load(W + cols, mask=mask).to(tl.float32)
    tl.store(Y + row * stride_y + cols, x * tl.rsqrt(ms + eps) * (1.0 + w), mask=mask)

You can let the CLI draft annotations from parameter names and data flow. A wrong draft can only make verification fail, never pass:

theformalera annotate kernels/act_new.py

kernels/act_new.py:6 silu_and_mul  (sigmoid)
╭────────────────────────────────────────────────────────────────────────╮
│ @tfe.implements("Qwen/Qwen3.8-27B@1.0:layers[*].mlp.act", grid=("T",), │
│                 bind={'gate_up': 'gate_up', 'out': 'y'})               │
╰────────────────────────────────────────────────────────────────────────╯
A wrong draft can only make verification fail, never pass.

See Annotate Triton kernels for every parameter.

Scan

theformalera scan

Found 5 annotated kernels (5 Triton)
  kernels/act.py:13          silu_mul_kernel         -> layers[*].mlp.act
  kernels/act_fast.py:18     silu_mul_tanh_kernel    -> layers[*].mlp.act   (autotune: 4 configs)
  kernels/attn_decode.py:28  paged_decode_attention  -> layers[*].attn.core
  kernels/norm.py:14         rmsnorm_kernel          -> layers[*].input_norm, layers[*].post_attn_norm
  kernels/residual.py:13     residual_add_kernel     -> layers[*].attn_residual
Coverage Qwen/Qwen3.8-27B@1.0: 5 of 21 graph nodes
  not covered: embed, gdn.in_proj, gdn.conv, gdn.core, gdn.norm, gdn.out_proj, mlp.gate_up, mlp.down,
mlp_residual, attn.qkv_proj, attn.qk_norm, attn.rope, attn.gate, attn.o_proj, final_norm, lm_head

scan never imports your code; it reads annotations from the source. A kernel under require_annotation without an annotation is listed here, and it fails verify.

Verify

theformalera verify

 kernel                   spec node                  configs   result    level / id     time
 ───────────────────────────────────────────────────────────────────────────────────────────
 silu_mul_kernel          layers[*].mlp.act              1/1   PASS      PROVED         2.9s
 silu_mul_tanh_kernel     layers[*].mlp.act              4/4   PASS      PROVED        14.1s
 paged_decode_attention   layers[*].attn.core            0/1   FAILED    F-0001         1.8s
 rmsnorm_kernel           layers[*].input_norm           1/1   PASS      PROVED         3.3s
 rmsnorm_kernel           layers[*].post_attn_norm       1/1   PASS      PROVED         3.6s
 residual_add_kernel      layers[*].attn_residual        1/1   PASS      PROVED         3.3s

5 passed · 1 failed · 0 unknown        run `theformalera explain F-0001`
lemma hub: 14 hits (14 built-in) · 1 new → acme

The tanh-based SiLU kernel computes the sigmoid in a different way. Its proof needed a sub-proof no lemma covered, so the engine searched, found one, and deposited it as a new lemma. lemma preview shows where it goes:

theformalera lemma preview

contribution policy: contribute = "org" · runner local · snapshot 2026-11-01T04:10Z
L-d07f2c  general-level  →  acme library (org)
  ∀ (a0 a1 : ℝ), a0 * a1 * (1/2) + a0 * a1 * tanh (a0 * (1/2)) * (1/2) = a0 * a1 * (1 + exp (-a0))⁻¹
  first solved in 559ms by `tanh_eq_exp; exp_neg; field_simp; ring_nf` · nodes Qwen/Qwen3.8-27B:mlp.act
submitted as D-76ec659a2f: queued for the Hub-side Lean re-check (admission)
lemma statements reference only Mathlib — never kernel names, file paths, repository names or annotation
contents

Explain and reproduce the failure

theformalera explain F-0001
theformalera repro F-0001 -o repro.py

repro.py

# generated by: theformalera repro F-0001
# paged_decode_attention -> Qwen/Qwen3.8-27B@1.0:layers[*].attn.core
# witness (typical): B=1, seq_len=17  ·  o[0, 0, 0]: kernel -0.163625, spec -0.17983
import torch
import theformalera as tfe
from kernels.attn_decode import paged_decode_attention

case = tfe.load_case("F-0001", witness="typical")              # concrete input with B=1, seq_len=17
paged_decode_attention[case.grid](**case.kernel_args, D=256, G=6, PAGE=16)                   # runs on the GPU
out = case.output("o")
ref = tfe.spec_eval(case.spec_key, **{k: case.spec_args[k] for k in ['q', 'k', 'v', 'seq_lens']})  # float64
print("max abs diff:", (out.double() - ref).abs().max().item())

On an RTX 4090 the repro prints max abs diff: 0.42601415461163633. With --witness minimal (seq_len=1) it prints nan.

Fix and re-verify

Apply the fix that explain suggested:

kernels/attn_decode.py

-    n_pages = seq_len // PAGE_SIZE
+    n_pages = tl.cdiv(seq_len, PAGE_SIZE)

theformalera verify kernels/attn_decode.py

 kernel                   spec node             configs   result    level / id      time
 ───────────────────────────────────────────────────────────────────────────────────────
 paged_decode_attention   layers[*].attn.core       0/1   UNKNOWN   unsupported     1.7s

0 passed · 0 failed · 1 unknown

The counterexample is gone and the safety checks pass, but the engine cannot prove online-softmax paged attention yet (see Limitations). So the result is UNKNOWN: never a PASS. By default, UNKNOWN fails CI.

Waive what cannot be decided yet

A waiver needs an owner and an expiry date:

theformalera.toml

[[waiver]]
id      = "W-1"
kernel  = "paged_decode_attention"
verdict = "unknown"
reason  = "paged online-softmax lemma pending; no counterexample, safety checks pass"
owner   = "alice"
expires = 2026-11-30

 paged_decode_attention   layers[*].attn.core            0/1   UNKNOWN   waived       cached

5 passed · 0 failed · 1 unknown · 1 waived

Unchanged kernels are served from the results cache. Every active waiver is written into the release certificate.

Gate CI

.github/workflows/theformalera.yml

name: theformalera
on:
  pull_request:
  push:
    branches: [main]

jobs:
  verify:
    runs-on: ubuntu-latest        # no GPU needed
    permissions:
      contents: read
      pull-requests: write
      security-events: write
    steps:
      - uses: actions/checkout@v4
      - uses: theformalera/verify-action@v1
        with:
          token: ${{ secrets.THEFORMALERA_TOKEN }}
          changed-only: ${{ github.event_name == 'pull_request' }}

Make theformalera / verify a required check. See Continuous integration.

Sign off a release

theformalera guards                                    # runtime checks of every assumption
theformalera verify > /dev/null                        # sign-off needs a whole-project run
theformalera signoff --model Qwen/Qwen3.8-27B@1.0 --yes
theformalera cert verify release.cert.json --require L1 --pubkey .theformalera/signing-key.pub

coverage L1 · nodes 6/21 · 6 kernels · scenarios —
  lemma closure: 1 lemma(s) (0 public · 1 org · 0 local) + built-ins of the spec package · proofs/lemmas/
✓ signed certificate -> release.cert.json  (proofs in proofs)
✓ certificate valid · Qwen/Qwen3.8-27B@1.0.0 · sm_90a · level L1 · 6 kernels

The certificate is a signed in-toto statement. The proofs and the Lean sources of every lemma they use ship next to it. See Release sign-off.

Get started

Concepts

Guides

Model conformance

Case studies

Help

Tutorial: onboard a repository