Python API

import theformalera as tfe

tfe.implements

The annotation decorator; see Annotation reference.

tfe.layout

The layout constructors (tfe.layout.paged_kv(…), …); see Annotation reference.

tfe.annotations_of

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

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

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

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.

theformalera.trace.record_launch

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

CLI

Configuration

Formats

tfe.implements

tfe.layout

tfe.annotations_of

tfe.load_case

tfe.spec_eval

tfe.gym

theformalera.trace.record_launch

tfe.version

​tfe.implements

​tfe.layout

​tfe.annotations_of

​tfe.load_case

​tfe.spec_eval

​tfe.gym

​theformalera.trace.record_launch

​tfe.version

tfe.implements

tfe.layout

tfe.annotations_of

tfe.load_case

tfe.spec_eval

tfe.gym

theformalera.trace.record_launch

tfe.version