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

# Annotate CUDA and CUTLASS kernels

> Comment or macro annotations for C++ kernels, template instances, and what the engine does with them today.

C++ annotations are comments, so they need no build-system changes and add no link-time dependency. They attach to the next declaration.

```cpp csrc/gemm_sm90.cu theme={"system"}
// @theformalera implements  = "Qwen/Qwen3.8-27B@1.0:layers[*].mlp.gate_up"
// @theformalera bind        = { A: x, B: w_gate_up, D: gate_up }
// @theformalera layout      = { A: row_major(T, 5120), B: col_major(5120, 34816), D: row_major(T, 34816) }
// @theformalera domain      = { T: [1, 262144] }
// @theformalera instantiate = GateUpGemm<Shape<_128,_256,_64>, KernelTmaWarpSpecializedCooperative>
//                             GateUpGemm<Shape<_64,_128,_64>,  KernelTmaWarpSpecialized>
template <class TileShape, class Schedule>
struct GateUpGemm { /* CUTLASS 3.x GemmUniversal ... */ };
```

A value can continue on the following comment lines. Indent them.

## Fields

| Field | Required | Meaning |
| - | - | - |
| `implements` | yes | One or more Spec Keys, in double quotes |
| `bind` | no | `{ kernel_param: spec_name, … }` |
| `layout` | no | `{ param: row_major(dims…) \| col_major(dims…), … }` |
| `domain` | no | `{ T: [lo, hi], … }`; only narrows |
| `assume` | no | Preconditions, as for Triton |
| `grid` | no | The launch grid, for kernels that are not standard CUTLASS GEMM templates |
| `instantiate` | no | Template instances to verify; one per line. Without it, the explicit instantiations in the file are used. |

Templates must be instantiated to be verified: list the instances you actually deploy.

## Macro form

Teams that prefer macros can include the header shipped with the package (installed under `<prefix>/include`):

```cpp theme={"system"}
#include <theformalera/annotate.h>

THEFORMALERA_IMPLEMENTS("Qwen/Qwen3.8-27B@1.0:layers[*].mlp.gate_up");
template <class TileShape, class Schedule>
struct GateUpGemm { ... };
```

Every macro (`THEFORMALERA_IMPLEMENTS`, `THEFORMALERA_BIND`, `THEFORMALERA_LAYOUT`, `THEFORMALERA_DOMAIN`, `THEFORMALERA_ASSUME`, `THEFORMALERA_INSTANTIATE`, `THEFORMALERA_GRID`) expands to nothing.

## Scan configuration

```toml theformalera.toml theme={"system"}
[scan]
include = ["kernels/**/*.py", "csrc/**/*.cu", "csrc/**/*.cuh"]

[targets]
cutlass = { arch = ["sm_90a"], include = ["third_party/cutlass/include"] }
```

`theformalera init` detects CUTLASS checkouts under `third_party/cutlass/include` or `cutlass/include` and fills in `include` for you.

## What you get today

> [!WARNING]
>
> Device-IR lifting for CUTLASS and CuTe is on the Phase 2 roadmap. A CUTLASS instance is reported **UNKNOWN** today, never PASS.

Even so, annotating CUTLASS kernels is worth it now:

* `scan` and `coverage` count them, so you can see which graph nodes have an implementation;
* `trace` records their launches (`THEFORMALERA_TRACE_LAUNCH`, or `theformalera.trace.record_launch` from a PyTorch extension) for L3 sign-off;
* when [Volta](https://github.com/francois141/ptx_verifier) is available, the PTX of each instance is checked for data races and sampled equivalence. A numerically confirmed Volta rejection is a genuine `FAILED`, and an acceptance is attached as evidence.

For CUTLASS kernels in CI, run the job in a CUDA devel container (`nvidia/cuda:<version>-devel-ubuntu22.04`) so that `nvcc` is available. No GPU is needed.


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