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

# RL environment

> Use the verifier as the reward gate when training models to write kernels.

`theformalera.gym` turns a spec node into a task. The policy writes a Triton kernel, the engine verifies it, and only verified kernels earn a reward.

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

env  = tfe.gym.make("Qwen/Qwen3.8-27B@1.0:layers[*].input_norm", target="sm_90a", lang="triton")
task = env.reset()                 # Lean 4 spec, constants, shape domain, signature, prompt
res  = env.step(kernel_source)     # verification runs on the CPU
res.verdict, res.counterexample, res.latency_us, res.reward
res.lemma_hits, res.lemma_saved_s  # rollouts of one task share sub-proofs through the Lemma Hub
```

Run it inside a project that locks the model (`theformalera pull`); the environment verifies against the locked specs.

## The task

`env.reset()` returns a `Task`:

| Field | Contents |
| - | - |
| `key`, `target`, `lang` | The Spec Key, the target architecture, `triton` |
| `kernel_name`, `signature` | The function the policy must define, e.g. `def kernel(X, W, Y, eps, H: tl.constexpr, BLOCK: tl.constexpr):` |
| `annotation` | The `@tfe.implements(...)` the environment attaches |
| `spec` | `spec.get` output: Lean definition, formula, constants, tensors, domains |
| `prompt` | A ready-made prompt with all of the above |

## The step

`env.step(source)` removes any `@tfe.implements` the policy wrote, attaches the environment's annotation to `@triton.jit def <kernel_name>`, and verifies the result.

| `StepResult` field | Meaning |
| - | - |
| `verdict`, `kind` | `PASS` / `FAILED` / `UNKNOWN` and the subtype |
| `counterexample`, `holds_when` | The typical witness and the failing region, for FAILED |
| `latency_us` | From your `perf` callback, measured on your GPU; `None` without one |
| `reward` | See below |
| `lemma_hits`, `lemmas_new`, `lemma_saved_s` | Lemma Hub activity of the rollout |
| `raw` | The full result JSON |

## Rewards

* **Correctness is a gate, not a bonus.** FAILED and UNKNOWN earn `0`. UNSAFE earns `unsafe_reward` (default `0`; set it negative to penalise).
* A PASS earns `1.0`, or `1 / latency_us` when you pass `perf=`:

```python theme={"system"}
env = tfe.gym.make(key, level="quick", unsafe_reward=-1.0, perf=lambda src: benchmark_on_gpu(src))
```

## Why it resists reward hacking

* The annotation, the shape domain and the assumptions belong to the environment. The policy writes only the kernel body, so it cannot narrow the domain to "prove" a wrong kernel.
* A proof holds for every input in the domain, so tampering with test inputs gains nothing.
* The policy cannot write lemmas. Lemmas are extracted by the engine, only from proofs that passed the Lean check.

[Reward hacking](https://docs.theformalera.com/case-studies/reward-hacking.md) shows three rollouts that pass an `allclose` reward check and are all rejected by the spec gate.

## Throughput

* Use `level="quick"` (the default) for dense signals, and `level="proof"` for the final candidates.
* Rollouts of the same task share the project's results cache and lemma base, so a sub-proof one rollout pays for is a hit for the next ones.


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