Annotate CUDA and CUTLASS kernels

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

csrc/gemm_sm90.cu

// @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):

#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

theformalera.toml

[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

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

Get started

Concepts

Guides

Model conformance

Case studies

Help

Annotate CUDA and CUTLASS kernels

Fields

Macro form

Scan configuration

What you get today

​Fields

​Macro form

​Scan configuration

​What you get today

Fields

Macro form

Scan configuration

What you get today