Lean RL Environments from a Production Cryptography Formal Verification

We provide 1,569 Lean 4 proof completion tasks across 11 RL environments packaged in Harbor format. Tasks feature 0/1 reward and programmatic grader based on the Lean kernel and Lean comparator that defends against reward hacking. These tasks are drawn from a 2.5M+ line private formal verification of OpenVM, a production zero-knowledge proof system created by our in-house cryptography experts.

Difficulty for frontier models ranges from pass@1 around 30% on small tasks to sub-5% on long horizon benchmarks. On a 24-task sample set from Environment D (Coding Theory and Proximity Testing) and E (Production Verifier Equivalence), frontier models have scores indicating trainable gradient.

Eval results: pass@1 over 8 attempts per task, 90-minute timeout and maximal thinking settings.
Loading results…

The tasks cover both cryptographic soundness and implementation correctness. We divide them into difficulty levels based on the number of lines in the ground truth proof.

Statistics on available RL environments and tasks. See more at Environment Descriptions.
Domain	Environments	Lines of Lean	All tasks	S	M	L	XL	XXL
Loading summary…

Task and Environment Construction

Our tasks were created by Intrinsic’s team of PhD experts, including former faculty members from UChicago and MIT, IMO/IOI gold medal winners, and production cryptographers. The data is from our real-world formal verification of OpenVM, a zero-knowledge virtual machine developed by Intrinsic (d.b.a. Axiom). All data is proprietary and has not appeared in any public corpus.

Each task presents the agent with a prompt specifying a target theorem statement to prove and a set of definitions necessary to state the target theorem. The agent is also provided with the list of allowed MCP tools. Each task also ships with a reference oracle, never visible to the agent, that can restore the pristine proof of the theorem for validation.

Tasks are generated from production formalization repos according to the following pipeline: given a target theorem, we construct a task by replacing its proof with sorry, and pruning all definitions not in the dependency tree of the target and all other theorem/lemma statements and proofs. The agent must return the directory with the sorry replaced by a proof that the Lean kernel accepts, without changing the statement, using sorry, or introducing non-standard axioms.

Tasks are in Harbor format with Lean v4.34.0 and Mathlib v4.34.0. Network egress during the agent phase is restricted to Lean Loogle and the agent’s model API. The agent receives two MCP tools from the Lean LSP toolset, lean_run_code and lean_loogle (the tasks are private, so no task data is present in the Loogle index).

Select a target theorem and replace its proof with sorry
Drawn from the production formalization of OpenVM.
Prune all other theorems/lemmas and out-of-tree definitions
Statements and proofs of all other theorems/lemmas, and every definition outside the target theorem’s dependency tree.
Package as a Harbor task
Docker on Lean v4.34.0 with the matching Mathlib pin; lean_run_code and lean_loogle over MCP; egress limited to the Loogle host and the agent’s model API.
Agent returns the task directory
With the sorry replaced by a proof, the statement untouched, and no non-standard axioms.
Grading with 0/1 reward
The grader checks proof correctness with the Lean kernel and statement integrity with the Lean comparator. A submission scores 1 only if it passes both checks.

Reward and Grading

The RL environments are scored with 0/1 reward based on a custom, two-tier grader using both the Lean kernel and the Lean comparator [The Lean FRO, 2025] to defend against adversarial behavior. The two tiers of the grader ensure proof correctness and statement integrity, respectively.

Tier 1 — proof correctness

This phase of the grader checks that the target module with proof compiles without sorry and passes the Lean kernel. Specifically, it checks:

No existing .lean file in the task directory other than the one containing the target theorem was modified by the agent. The agent is allowed to introduce new .lean files.
The agent solution does not contain sorry, admit, or axiom.
The solution builds, as checked by lake build <module> returning exit code 0.

Tier 2 — statement integrity

To protect against reward hacking by tampering with the statement of the target theorem, we apply the gold standard Lean comparator to check the following statement integrity conditions, which ensure the proved theorem in the solution matches the original theorem in the task and exclude forbidden tactics like native_decide:

The target theorem in the solution has elaborated type matching the original target.
The target theorem in the solution has transitive axioms contained only in the allowlist [propext, Classical.choice, Quot.sound].

A submission scores 1 only if it passes both grading tiers. Tier 1 is used for fast feedback, and Tier 2 is present to protect against adversarial agent behavior.

Environment Descriptions

The tasks form 11 environments spanning cryptographic soundness and implementation correctness proofs for OpenVM. Each environment is a sequence of intermediate results building to a top-level theorem, and each theorem or lemma comes with a ground truth proof.

We measure task size by the number of lines of Lean in the ground truth proof of the target theorem, including all dependencies in the same environment. We divide tasks into five size classes:

S (task size 500–1,000 lines)
M (task size 1,000–2,500 lines)
L (task size 2,500–5,000 lines)
XL (task size 5,000–10,000 lines)
XXL (task size >10,000 lines)

Environment	Lines of Lean	S	M	L	XL	XXL
Loading distribution…

Contamination and Versioning

Canaries are embedded in all tasks. The underlying data is proprietary and has not appeared in any public corpus. The RL environments are built on Lean v4.34.0 and Mathlib v4.34.0.