> ## 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. # Tutorial: onboard a repository > From an unannotated set of Triton kernels to a gated CI check and a signed release certificate. 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](https://docs.theformalera.com/quickstart.md) shows how to set up the local Hub these commands use. **1. Initialise the project** Run `init` at the repository root. It finds Triton and CUDA code and writes `theformalera.toml`: ```bash theme={"system"} theformalera init --model Qwen/Qwen3.8-27B ``` ```text theme={"system"} ✓ 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: ```toml theformalera.toml theme={"system"} [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](https://docs.theformalera.com/guides/coding-agents.md). **2. Pull and lock the specs** ```bash theme={"system"} theformalera pull ``` ```text theme={"system"} ✓ Qwen/Qwen3.8-27B@1.0.0 sha256:313a42af237f… signed theformalera (verified) wrote theformalera.lock (1 spec) ``` ```toml theformalera.lock theme={"system"} # 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`. **3. Read the spec of the node you implement** ```bash theme={"system"} theformalera spec show 'Qwen/Qwen3.8-27B@1.0:layers[*].input_norm' ``` ```text theme={"system"} 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`. **4. 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: ```python kernels/norm.py theme={"system"} 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: ```bash theme={"system"} theformalera annotate kernels/act_new.py ``` ```text theme={"system"} 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](https://docs.theformalera.com/guides/annotate-triton.md) for every parameter. **5. Scan** ```bash theme={"system"} theformalera scan ``` ```text theme={"system"} 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`. **6. Verify** ```bash theme={"system"} theformalera verify ``` ```text theme={"system"} 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: ```bash theme={"system"} theformalera lemma preview ``` ```text theme={"system"} 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 ``` **7. Explain and reproduce the failure** ```bash theme={"system"} theformalera explain F-0001 theformalera repro F-0001 -o repro.py ``` ```python repro.py theme={"system"} # 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`. **8. Fix and re-verify** Apply the fix that `explain` suggested: ```diff kernels/attn_decode.py theme={"system"} - n_pages = seq_len // PAGE_SIZE + n_pages = tl.cdiv(seq_len, PAGE_SIZE) ``` ```bash theme={"system"} theformalera verify kernels/attn_decode.py ``` ```text theme={"system"} 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](https://docs.theformalera.com/concepts/limitations.md)). So the result is UNKNOWN: never a PASS. By default, UNKNOWN fails CI. **9. Waive what cannot be decided yet** A waiver needs an owner and an expiry date: ```toml theformalera.toml theme={"system"} [[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 ``` ```text theme={"system"} 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. **10. Gate CI** ```yaml .github/workflows/theformalera.yml theme={"system"} 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](https://docs.theformalera.com/guides/ci.md). **11. Sign off a release** ```bash theme={"system"} 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 ``` ```text theme={"system"} 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](https://docs.theformalera.com/guides/release-signoff.md). This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.