Rain improves software proof success with smarter agent design
RAIN: Agentic Proof Generation for Rocq-based Software Verification
Logic in Computer Science
Summary
Checking that software works correctly can be done by writing proofs, but making these proofs is very hard and slow. The authors created Rain, a smart assistant that helps write these proofs more easily by searching for useful facts, improving whole scripts, and learning from errors. They tested Rain on a set of software proofs and it worked much better than earlier tools, solving over 90% of problems. Rain also does this more cheaply than other general coding assistants.
What this means in practice
- •For software verification engineers: Automatically generate correct proofs for software using Rocq with higher success and efficiency.
- •For formal methods teams: Reduce manual effort in creating formal proofs by employing an agent that iteratively refines verification scripts.
Authors
Jinyi Zhou, Zenan Li, Yuan Yao, Jun Ma, Taolue Chen, Xiaoxing Ma
Abstract
Interactive theorem provers can provide strong correctness guarantees for software, but constructing the proofs remains a challenging and labor-intensive task. Inspired by the recent progress of modern coding agents, we present RAIN, a lightweight proof-specialized agent for Rocq proof generation. RAIN augments an LLM with proof engineering capabilities, including repository exploration, iterative refinement, and checker feedback. This design allows the agent to retrieve lemmas autonomously, revise complete proof scripts instead of isolated tactics, and iteratively refine its proof strategy using enriched proof-state information. Evaluated on a subset from CoqStoq, RAIN shows substantial improvements over the existing baselines, achieving over 90% prove success rate with at least 24.7% improvements. We also compare with general-purpose coding agents, the results show that RAIN maintains comparable prove success rate but with significant lower cost.