EasyProver scales up automated proofs for realistic code verification
Scaling Lean Theorem Proving for Real-World Code Verification
Computation and LanguageArtificial IntelligenceLogic in Computer ScienceSoftware Engineering
Summary
Verifying that computer programs are correct is very hard, especially with real-world details like how numbers behave and how code can fail. The authors created EasyProver, a system that can automatically prove or refute many code verification problems quickly and accurately using smart techniques like working in parallel and isolating parts of the problem. They also built Aegis, which turns competitive programming problems into more difficult tests involving real implementations, producing lots of examples of verified Rust and Lean programs. This work helps make automatic checking of complex code more practical for software developers.
What this means in practice
- •For software verification teams: Automatically check real-world Rust code correctness through scalable formal proofs incorporating low-level program details.
- •For reinforcement learning engineers: Use the verified Rust-Lean problem pairs as benchmark rewards to train and evaluate provers based on learning algorithms.
Authors
Debargha Ganguly, Divya Raghunathan, Dejan Jovanović, Vikash Singh, Soonho Kong, Aaron Tomb, Aman Goel, Ferhat Erata, Sam Bayless
Abstract
We present EasyProver, a Lean proving system built from recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service. Using an off-the-shelf frontier model with no additional training, it proves 669/672 PutnamBench problems and all six IMO 2026 formalizations and resolves 597/600 NTP4VC verification conditions and all 189 VERINA tasks by proof or refutation. Because these benchmarks are close to saturation, we also introduce Aegis, which converts competitive programming problems into much harder verification tasks over real implementations. The pipeline writes safe Rust solutions, translates them into Lean with Aeneas, generates specifications, and labels each frozen statement with a kernel-checked proof or refutation. It produces 2,045 differentially validated Rust-Lean program pairs and 11,533 candidate specifications. Unlike hand-written benchmarks, these tasks carry implementation-level obligations from fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation. On a stratified sample of 2,000 statements, EasyProver proves 1,054 (52.7%) within a 30-minute budget per statement. The same tasks can also be used to benchmark other provers and as rewards for reinforcement learning.