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

# Python API

> The public Python interface of the theformalera package.

```python theme={"system"}
import theformalera as tfe
```

## tfe.implements

The annotation decorator; see [Annotation reference](https://docs.theformalera.com/reference/annotations.md).

## tfe.layout

The layout constructors (`tfe.layout.paged_kv(…)`, …); see [Annotation reference](https://docs.theformalera.com/reference/annotations.md#python-tfe-layout).

## tfe.annotations\_of

```python theme={"system"}
tfe.annotations_of(obj) -> tuple[tfe.Annotation, ...]
```

The annotations attached to a live kernel or launcher, for tools that import kernel modules. Each `Annotation` has `keys`, `grid`, `bind`, `layout`, `domain`, `assume`, `configs` and `level`.

## tfe.load\_case

```python theme={"system"}
tfe.load_case(fid: str, witness: str = "typical", root: Path | None = None, device: str | None = None) -> LoadedCase
```

Rebuild the concrete input of a counterexample from the last run (`.theformalera/last-run.json`). `witness` is `"typical"` or `"minimal"`. Tensors are created on `device` (default: `cuda` if available, else `cpu`), in the kernel's dtypes; paged inputs are laid out through a shuffled block table.

| `LoadedCase` | |
| - | - |
| `id`, `spec_key`, `shape` | The failure id, its Spec Key, and the values of the shape symbols |
| `grid` | The launch grid, ready for `kernel[case.grid](…)` |
| `kernel_args` | Keyword arguments for the kernel: input tensors, empty output tensors, scalars |
| `spec_args` | The logical inputs as float64 tensors, for `spec_eval` |
| `constexprs` | The constexpr values of the failing config |
| `output(name=None)` | An output tensor written by the kernel, reshaped to its logical shape, as float64 on the CPU |

## tfe.spec\_eval

```python theme={"system"}
tfe.spec_eval(spec_key: str, root: Path | None = None, **spec_args) -> torch.Tensor | dict[str, torch.Tensor]
```

Evaluate a spec node with the float64 reference interpreter of the locked spec package. It returns one tensor for single-output nodes and a dict otherwise.

## tfe.gym

```python theme={"system"}
env = tfe.gym.make(key, target="sm_90a", lang="triton", level="quick", unsafe_reward=0.0, perf=None,
                   kernel_name=None, grid=None, bind=None, configs=None, root=None)
task = env.reset()
res = env.step(kernel_source)
```

See [RL environment](https://docs.theformalera.com/guides/rl-environment.md).

## theformalera.trace.record\_launch

```python theme={"system"}
from theformalera.trace import record_launch

record_launch(kernel: str, grid: tuple[int, ...], tensors: dict[str, torch.Tensor],
              scalars: dict | None = None, module: str = "extension") -> None
```

Record a launch of a non-Triton kernel (a CUDA or CUTLASS extension) while `theformalera trace` is recording. Outside a trace it does nothing.

## tfe.**version**

The CLI and SDK version, for example `"0.9.0"`.


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