EasyProver: How Recursive Agents Tackle Formal Verification of Real-World Code

Formal verification has long remained confined to academic benchmarks and small-scale examples. Verifying real-world code, however, has been difficult to scale due to state-space explosion and complex implementation details. EasyProver attempts to bridge this gap with a Lean proof system driven by recursive agents—it does not rely on specially trained models, using only off-the-shelf frontier models to achieve near-perfect scores on multiple benchmarks approaching saturation, while simultaneously introducing Aegis, a new benchmark targeting real implementations.

How the System Works: Isolated Contexts and Asynchronous Search

At the core of EasyProver is a set of recursive agents, each with an isolated context. This design allows proof search to branch without cross-contamination, avoiding information interference in long contexts. Combined with asynchronous search and parallel tactic probing, the system can explore multiple proof paths simultaneously; an elastic elaboration service expands compute resources as needed, ensuring proof checking is not bottlenecked at a single point.

The key judgment behind this architecture is: rather than fine-tuning models to adapt to the proof assistant, shift the engineering focus to the orchestration layer—letting multiple agents with limited individual capabilities explore in parallel and recursively, then relying on Lean's kernel for strict checking to filter results. The paper notes that the system "uses off-the-shelf frontier models with no additional training," which significantly lowers the barrier to reproducing EasyProver.

Lean and Tactic Probing

Lean is an interactive theorem prover led by Microsoft Research, and also a dependently typed programming language. It is used by mathematicians to formalize theorems and by engineers to verify program correctness. Similar to Coq/Isabelle, a Lean proof is essentially a term checked by the kernel, and mathematicians often use tactics to construct proofs step by step in a way closer to human reasoning. Elaboration refers to the process of expanding surface syntax written by users, inferring implicit arguments, and filling in type information to ultimately generate a kernel-checkable term; it is often compute-intensive and prone to becoming a bottleneck. So-called "parallel tactic probing" means trying multiple tactics simultaneously on a proof path (such as induction, simplification, and automated solving), evaluating their returns in parallel before choosing the best to advance. Combined with Lean's strict kernel checking, this strategy keeps the search process efficient while ensuring every step can be reliably verified.

Benchmark Results: From PutnamBench to VERINA

According to the paper's data, EasyProver proved 669/672 problems on PutnamBench, completed all six IMO 2026 formalized problems, and solved 597/600 verification conditions on NTP4VC. It also completed all 189 tasks in VERINA, using both proof and disproof approaches.

These numbers send a clear signal: traditional competition mathematics and some program verification benchmarks are approaching saturation. When a proof system can pass at such a high rate, the benchmark itself has little discriminative power left. The authors explicitly state that these benchmarks are "approaching saturation," which is precisely the direct motivation for building a new benchmark. The disproof path is also noteworthy—the system can not only construct proofs but also produce counterexamples accepted by the kernel, which is crucial for judging the validity of verification conditions.

Aegis: Turning Competition Problems into Verification Tasks for Real Implementations

The construction pipeline of Aegis is quite ingenious engineering. It first transforms competitive programming problems into harder verification tasks targeting real implementations: the pipeline writes safe Rust solutions, translates them into Lean via Aeneas, then generates specifications, and finally annotates each frozen statement with a kernel-checked proof or disproof.

In terms of output scale, Aegis generated 2,045 differentially verified Rust-Lean program pairs and 11,533 candidate specifications. The biggest difference from handwritten benchmarks is that these tasks carry implementation-level obligations: fixed-width arithmetic, explicit failures, generated loops, type casts, and functionalized mutable state. In other words, verifiers must confront the corners of real code that textbooks tend to ignore.

Aeneas and Rust-Lean Differential Verification

Aeneas is a tool that translates Rust programs into Lean functional models, developed by Microsoft Research and other institutions for formal reasoning about real system code. It translates Rust's ownership, borrowing, and mutable state into pure functional Lean definitions, enabling verifiers to discuss program behavior in a theorem prover. So-called "differential verification" means retaining both the Rust source code and its Lean model and checking that the two agree on observable behavior; in the Aegis pipeline, the pipeline also generates specifications for each frozen statement and annotates them with kernel-checked proofs or disproofs. This dual representation makes the tasks close to real implementations while being mechanically checkable in Lean, thereby compensating for the shortcomings of handwritten benchmarks that often ignore implementation-level obligations (such as fixed-width arithmetic and explicit failures).

Performance on Real Code and Future Uses

On a stratified sample of 2,000 statements, EasyProver proved 1,054 within a 30-minute per-statement time budget, accounting for 52.7%. The paper describes these tasks as "much harder" than competition benchmarks—a drop from near-perfect scores to slightly above half precisely shows that Aegis has not been easily cracked by existing methods.

The authors note that this batch of tasks has two additional uses: first, as a benchmark to evaluate other provers; second, as a reward signal for reinforcement learning. The former means the community has an evaluation arena that is hard to saturate; the latter points to a path of self-improvement—using kernel-checked proofs and disproofs as verifiable rewards to train stronger proof agents.

Verifiable Rewards and Reinforcement Learning

The kernel checking results of formal proofs naturally constitute a kind of "verifiable reward": a proof passing is a positive example, and a disproof being accepted is a negative example, with no need for human annotation or reward models. Unlike RLHF, which relies on human preferences, this reward signal is mechanically determined by the Lean kernel and is nearly impossible to forge. Using such signals for reinforcement learning to train proof agents has been an important direction in theorem proving in recent years—models can autonomously generate many attempts, which are then filtered by the kernel, enabling continuous self-improvement without supervised data. The real implementation tasks provided by Aegis further extend this reward from competition mathematics to engineering code, bringing the training distribution closer to actual verification scenarios.

Engineering Significance and Points to Watch

The value of EasyProver lies not only in its scores but in demonstrating a scalable path that does not rely on specialized training: the combination of isolated contexts, asynchronous search, parallel probing, and elastic elaboration directs the reasoning capabilities of general models toward the high-barrier domain of formal proof. Aegis fills the gap on the evaluation side, giving "real implementation verification" a repeatable and extensible source of tasks.

It is worth noting that the 52.7% pass rate still leaves a large number of unsolved statements, and implementation details such as fixed-width arithmetic and explicit failures are precisely the difficulties. The system's performance on larger codebases and longer proof chains, as well as the quality distribution of specifications generated by Aegis, still require more independent analysis to examine.

One-line Summary

EasyProver uses recursive agents and off-the-shelf frontier models to achieve near-perfect scores on multiple benchmarks and introduces Aegis, a benchmark for real code verification.

Paragraph Summary

EasyProver is a Lean proof system driven by recursive agents, with core designs including isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service, and it does not rely on specially trained models. It proved 669/672 problems on PutnamBench, completed all six IMO 2026 formalized problems, solved 597/600 verification conditions on NTP4VC, and completed all 189 tasks in VERINA. Because these benchmarks are approaching saturation, the authors built Aegis: transforming competitive programming problems into verification tasks targeting real Rust implementations, producing 2,045 differentially verified Rust-Lean program pairs and 11,533 candidate specifications. On a sample of 2,000 statements, EasyProver proved 52.7% within a 30-minute budget per statement, showing that real implementation verification remains challenging while also serving as an evaluation arena and a reinforcement learning reward signal.