RL environment

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

​

The task

​

The step

​

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=:

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.

​

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.