> ## 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.

# Limitations

> What is out of scope by design, and what the engine cannot prove yet.

Stating the boundaries plainly is part of the product. When a kernel falls outside what the engine can prove, the result is UNKNOWN, never PASS.

## Out of scope by design

| Not verified | Notes |
| - | - |
| Floating-point rounding and associativity | Numbers are real numbers. Reordered sums, different tile sizes and different accumulation precision are the same function. Run-to-run differences from atomic accumulation order are out of scope too. |
| Everything below Triton IR | The Triton back end, LLVM, `ptxas` and the hardware are trusted. |
| The spec's reference implementation | If the official implementation is wrong, the spec inherits the error. See [Trust model](https://docs.theformalera.com/concepts/trust-model.md). |
| Host code outside traced scenarios | Schedulers, batching and samplers are only checked in the scenarios recorded for [L3 sign-off](https://docs.theformalera.com/guides/release-signoff.md), and that is sampling, not proof. |
| Performance | Use your own profiler. |
| Sparse models (MoE) | Only dense models are supported. |
| Non-text towers | The specs cover the text path only: no vision or audio encoders, no MTP head. |

## What the engine proves today

| Kernel shape | Result |
| - | - |
| Row kernels: RMSNorm and its variants, per-row norms with one tile per row | PROVED |
| Tiled loops that accumulate a reduction (`for b in range(0, N, BLOCK): acc += …`), and stores inside loops | PROVED |
| Element-wise kernels on flat or 2-D grids: SwiGLU / GeGLU activations, residuals, gates | PROVED |
| The same kernels lowered for AMD (`gfx942`, `gfx950`): ROCm math calls (`__ocml_tanh_f32`) are lifted like libdevice | PROVED |
| GEMM with a K loop (`acc = tl.dot(a, b, acc)`) | PROVED (linear nodes) |
| Online softmax, paged attention, the chunked delta rule | Counterexamples, overflow and safety are found; a correct kernel is UNKNOWN |
| CUTLASS / CuTe | Annotations are scanned; PTX evidence from Volta is attached; the result is UNKNOWN |
| Launcher-level annotations (on a Python wrapper) | Discovered and traced for L3; static verification reports UNKNOWN |
| Fused Spec Keys (`{attn_residual, post_attn_norm}`) | Bounded only: no fused closed form yet |
| Whole-layer and whole-model keys (`layers[*]`, `*`) | Reserved syntax |

Counterexamples (COUNTEREXAMPLE, UNSAFE, OVERFLOW, VACUOUS) are found for **every** kernel shape, including those the engine cannot prove. A bug is caught even when the correct version would only reach UNKNOWN.

### Which nodes can be PROVED

A proof needs a closed form of the node's Op Spec in the proof generator. In this release that covers:

| Op Spec | Nodes |
| - | - |
| `rmsnorm`, `rmsnormOffset`, `rmsnormUnit` | `input_norm`, `post_attn_norm`, `post_mix_norm`, `post_ffn_norm`, `final_norm`, per-head `attn.qk_norm` / `attn.v_norm` |
| `linear` | `attn.qkv_proj`, `attn.o_proj`, `mlp.gate_up`, `mlp.down`, `gdn.in_proj`, `gdn.out_proj` |
| `siluMul`, `geluMul` | `mlp.act` |
| `residual` (without a learned layer scalar) | `attn_residual`, `mlp_residual` |
| `sigmoidGate` | `attn.gate` |
| `rmsnormGated` | `gdn.norm` (per head: `w ⊙ x̂ ⊙ silu(z)`) |

For any other node (`attn.rope`, `attn.core`, `embed`, `lm_head`, `gdn.conv`, `gdn.core`, Gemma 4's `mlp_residual` with its layer scalar), a kernel with no counterexample ends UNKNOWN. So does a kernel with two output stores (a residual add fused with the next norm, which writes both the residual and the normalised row), and a value subgoal no lemma and no search entry closes (the norm computed as `exp(−½ · log v)`). Counterexample search, overflow and safety checks still run for these nodes.

### Why attention is UNKNOWN today

The algorithm-level theorems already exist in the spec library and are kernel-checked:

* `flashAttn_eq`: FlashAttention (online softmax, block skipping) equals the attention head of the spec;
* `chunkDeltaRule_eq`: the chunked (WY-form) gated delta rule equals the recurrence, for every chunk size;
* `online_softmax_rescale` and `splitKV_lse_merge` (built-in lemmas).

Wiring them into the proof generator, so that a kernel's lifted loop is matched against them, is the next milestone. Until then those kernels stay UNKNOWN, and you can [waive](https://docs.theformalera.com/guides/policy-and-waivers.md) them with an owner and an expiry date.

### CUTLASS

For CUTLASS and CuTe kernels, device-IR lifting is on the roadmap. Today the engine reports UNKNOWN. When [Volta](https://github.com/francois141/ptx_verifier) is available, it adds PTX-level evidence:

* A Volta `REJECT` that is numerically confirmed is a genuine FAILED (COUNTEREXAMPLE, or UNSAFE for a data race).
* A Volta `ACCEPT` is recorded as evidence in the result, never turned into a PASS: Volta itself does not claim soundness.

## Model-scale limits of conformance

[Model conformance](https://docs.theformalera.com/conformance/overview.md) runs the Lean oracle in float64. By default it uses a reduced-width configuration of the same architecture. The theorem `reduced_same_architecture` proves it has the same layer pattern, attention variants and norms as the checkpoint. A full-size run (`--full`) or the checkpoint cross-check (`--pretrained`) of a 30B model needs the model in float64 in memory: about 8 bytes per parameter, so roughly 250 GB.

## Roadmap

| Phase | Adds |
| - | - |
| 1 | Gated attention (prefill, paged decode, GQA), Gated DeltaNet (chunk and recurrent), split-K / split-KV; launcher-level static verification |
| 2 | CUTLASS 3.x GEMM templates, CuTe DSL, race checks for TMA and warp specialisation |
| 3 | Whole-graph verification of MegaKernels; published Lean semantics of Triton IR, so the translation can be checked too |


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.