Source-linked AI summary
RAIN: Agentic Proof Generation for Rocq-based Software Verification
Jinyi Zhou, Zenan Li, Yuan Yao, Jun Ma, Taolue Chen, Xiaoxing Ma
TL;DR
Formal verification offers machine-checkable correctness, but human proof engineering remains challenging and labor-intensive. RAIN makes Rocq proof generation an agentic workflow around an LLM, with evaluation showing strong results against prior provers and lower cost than general-purpose coding agents.
Problem
Human proof engineering requires developers to understand the program, prover, and proof techniques, and proof developments can rival or exceed implementation size.
Source: §1 · p. 1Method
RAIN treats Rocq proof generation as an agentic workflow in which an LLM explores repositories, constructs and repairs proofs, and uses structured proof-state feedback.
Source: §1 · p. 2, §4.2 · p. 5Results
RAIN solves 95.8% of theorems in PnVRocqLib and 90.3% in CoqStoq, improving Cobblestone and PALM by 42.3% and 24.7%, respectively, while maintaining comparable success at lower cost than coding agents.
Source: §1 · p. 2Takeaways & Limitations
Proof-specific agent design can make Rocq proof generation more effective and economical within the evaluated settings.
Source: §8 · p. 10Repository exploration still relies primarily on names, tokens, and source text, so the LLM often has to guess an identifier to locate a useful lemma.
Source: §6 · p. 9
Abstract
from arXiv · showhide
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.
1 Introduction
Formal verification offers machine-checkable correctness guarantees, but constructing proofs is labor-intensive and repository-level Rocq systems still face limitations in retrieval, repair, and feedback. RAIN treats proof generation as an agentic workflow and reports higher success than prior methods, with competitive success and lower cost than general-purpose coding agents.
Motivation
- Formal verification states desired behavior mathematically and establishes correctness with machine-checkable proofs, beyond assurance over selected executions, abstractions, or bug classes.The introduction motivates this stronger assurance for safety- and security-critical systems.Source: §1 · p. 1
- Proof construction remains labor-intensive because developers must connect implementations to specifications using ITP knowledge and proof techniques.Proof developments in large verification projects can be comparable to or substantially larger than the implementations they verify.Source: §1 · p. 1
- Repository-level proof generation remains difficult because whole-script generation, surface repair, tactic-by-tactic proving, and fixed retrieval each have limitations.Existing approaches can fail on local mistakes, semantic changes to proof ideas, long-proof trajectories, or decisive lemmas missed by retrieval.Source: §1 · p. 1
- Modern tool-using coding agents can inspect repository definitions and lemmas, edit proof scripts, invoke checkers, and refine attempts in project context.A general-purpose agent connected to Rocq alone still lacks feedback such as local goals, hypotheses, and errors in later branches.Source: §1 · pp. 1–2
Approach
- RAIN frames Rocq proof generation as agentic proof engineering, with the LLM exploring repositories, constructing and repairing proofs while a specialized system supplies workspace and structured proof-state feedback.The agent can retrieve lemmas autonomously, revise whole scripts, and iteratively refine its strategy; Rocq remains the trusted proof boundary.Source: §1 · p. 2
Evaluations
- RAIN solves 95.8% of theorems in PnVRocqLib and 90.3% in CoqStoq, improving Cobblestone and PALM by 42.3% and 24.7%, respectively.On sampled CoqStoq theorems, it also maintains comparable success while reducing monetary cost by 48.8% over Claude Code with DeepSeek-v4-flash and 17.3% over Codex with GPT-5.4.Source: §1 · p. 2
Contributions
- The paper identifies three contributions: an agentic proof-engineering formulation, state-aware feedback, and RAIN, which experiments show outperforms prior provers in proof-generation success.The feedback exposes goals and hypotheses, collects multiple errors in one checking pass, and structures the information for proof repair.Source: §1 · p. 2
2 Preliminaries
Rocq is an interactive theorem prover in which tactics transform goals while the system tracks proof state and checks the resulting script. A proof script is organized into parser-level sentences, including commands and branch markers.
Rocq proof state
- Rocq checks proof scripts against theorem statements and rejects errors such as unavailable lemma names, wrong rewrite directions, or unfinished branches.Tactics transform a focused goal into zero, one, or several new goals; local state includes branch hypotheses, while global context includes definitions and proven lemmas.Source: §2 · p. 2
Proof scripts
- A Rocq source file consists of parser-level sentences, including theorem declarations, Proof., tactic commands, bullets or braces, and Qed.Sentences usually end with a period, and bullets organize multiple subgoals; a bullet branch must ordinarily be completed before Rocq moves to the next sibling.Source: §2 · p. 2
3 Motivation and Design Choices
The paper identifies repository-level proof-generation gaps and maps them to RAIN design choices: autonomous retrieval, semantic repair, richer feedback, and whole-script editing. The design targets retrieval misses, proof-idea failures, missing state and branch errors, and long-range proof difficulties.
Autonomous lemma retrieval
- Existing prescriptive retrieval can omit decisive lemmas, while RAIN lets the LLM search and read repository files according to its proof ideas.Fixed top-k retrieval can exclude a useful lemma, and file-local context can miss lemmas elsewhere in the project.Source: §3 · pp. 2–3
Semantic proof repair
- Surface repairs handle local symptoms but not semantic failures such as an unsuitable induction choice or wrong proof method; RAIN uses checker feedback and internal states to revise the proof idea.The LLM can change an induction choice or switch methods rather than being limited to identifier, bullet, or tactic repairs.Source: §3 · p. 3
Feedback augmentation
- General-purpose agents lack local goals and hypotheses and see only the first error, while RAIN collects local state and multiple branch errors for a feedback packet.Figure 1 illustrates how omitted state complicates diagnosing rewrite failures and how an early branch error can hide later ones.Source: §3 · p. 3, Figure 1 · p. 3
Long-range proofs
- Tactic-by-tactic systems can struggle on long proofs because errors accumulate, search scores disfavor depth, and locally valid tactics may lead to unproductive decompositions.The cited seL4 neuro-symbolic prover reports around 20% success on 393 theorems with ground-truth proofs exceeding 10 lines, versus 77% average success.Source: §3 · p. 3
Whole-script editing
- RAIN permits complete proof-script edits, allowing the LLM to revise a global proof structure or plan as well as make local repairs.The strategy is not confined to tactic-by-tactic changes.Source: §3 · p. 3
4 Approach
RAIN wraps LLM proof construction in a repository-aware loop of inspection, editing, Rocq checking, and feedback. Its preprocessing workspace and two feedback mechanisms support proof refinement, while fine-grained validation checks that the final proof is accepted without changing the intended theorem or bypassing proof obligations.
4 Approach
- RAIN preprocesses Rocq projects into a workspace, then runs a search-read-edit-feedback loop in which the LLM explores repository material, edits whole proofs, and uses checker feedback to choose the next revision.The workflow lets the LLM control proof strategy while Rocq checks each candidate proof.Source: §4 · pp. 3–4
4.1 Preprocessing
- Preprocessing uses parser-level sentence boundaries to recover declarations and build lightweight indexes for relevant definitions and project lemma and theorem statements.The workspace supports searching names or source text, browsing file declarations, and reading source around promising lemmas or definitions.Source: §4.1 · p. 4
4.2 Local-State Collection
- Local-state collection recovers the goals and hypotheses immediately before a failing or proof-skipping sentence and returns them with the checker report.RAIN inserts a temporary proof-state query before the sentence and reruns the checker; the original source remains the proof attempt being repaired.Source: §4.2 · pp. 4–5
4.3 Multi-Error Collection
- Multi-error collection temporarily skips the failing branch so Rocq can check later branches and return several errors, each optionally paired with its local state.Collected branch errors can be addressed together and may reveal that an earlier decomposition is unhelpful; temporary admitting is only for feedback, not proof acceptance.Source: §4.3 · p. 5
4.4 Fine-Grained Validation
- Fine-grained validation accepts a generated proof only if Rocq checks the repository, the target theorem statement is unchanged, and the output adds no proof-skipping commands or new axiom-like declarations.These checks reject attempts that pass by proving a different theorem or bypassing the intended proof.Source: §4.4 · pp. 5–6
5 Evaluation
Across sampled Rocq benchmarks, RAIN outperforms recent automated provers and achieves success rates comparable to general-purpose coding agents at lower cost. The evaluation also examines its feedback modules, generalization to a recent project, and performance on longer proofs.
5.1 Experimental Setup
- The evaluation samples 100 CoqStoq theorems with project dependencies and conventions preserved, and separately samples 100 Parcas proofs for recent-project generalization.For agent evaluation, proof bodies are replaced with Admitted while theorem statements and project configuration remain; agents may not use proof-skipping constructs. Success is measured at pass@1 by default, with pass@k also reported.Source: §5.1 · p. 6
5.2 RQ1: Comparison with Automated Provers
- RAIN solves over 95% of PnVRocqLib targets and 84/93 CoqStoq tasks, gaining at least 42.3% over Cobblestone and 24.7% over PALM on the reported comparisons.Cobblestone solves 53.5%; PALM solves 61/93 after 40 trials, while RAIN solves 84/93 with one trial.Source: Table 1 · p. 7, Table 2 · p. 7, §5.2 · p. 7
5.3 RQ2: Comparison with General-purpose Coding Agents
- General-purpose coding agents perform well, but RAIN has higher success with weaker backends and significantly lower monetary cost or token usage across the tested combinations.With GPT-5.4, Codex has a slightly higher success rate; RAIN also shortens runtime except against Codex.Source: Table 3 · p. 7, §5.3 · pp. 7–8, Table 4 · p. 8
5.4 RQ3: Ablation Study
- Removing both feedback modules reduces pass@10 to 92.0% and trial success to 86.8%, while full RAIN lowers monetary cost by 25.6% and wall-clock time by 30.9%.Local-state collection has a clear effect on success; multi-error collection mainly reduces wasted repair cost.Source: §5.4 · p. 8, Table 5 · p. 9
5.6 Result Analysis
- The 100-target CoqStoq sample is dominated by short and medium proofs: 89 targets require at most 30 steps and 95 at most 50.Only five targets exceed 50 steps; RAIN solves all five at pass@10, but trial-level success falls from 95.7% on targets at or below 30 steps to 51.8% above 30.Source: §5.6 · pp. 8–9
5.5 RQ4: Generalization to a Recent Project
- On Parcas, RAIN solves 98/100 theorems at pass@10 with 93.3% trial success, and reduces monetary cost versus Claude Code and OpenCode.Compared with Claude Code, RAIN also reduces wall-clock time by 25.5%; versus OpenCode, by 6.8%.Source: §5.5 · p. 8, Table 6 · p. 9
5.6 Result Analysis
- All five remaining pass@10 failures in the 100-theorem sample come from the fourcolor development, whose proof style uses specialized Mathematical Components and ssreflect features.The authors identify boolean reflection, ssreflect views, canonical structures, coercions, and graph-coloring idioms as possible backend-model weak points.Source: §5.6 · p. 9
6 Discussion
The discussion identifies benchmark exposure and run-to-run variation as evaluation concerns, and notes that repository search remains primarily lexical. It also describes semantic retrieval as a possible extension.
Benchmark exposure
- The Parcas experiment reduces the likelihood of direct target-project exposure because the repository appeared after the evaluated DeepSeek model was released, but general proof-pattern exposure remains possible.The repository was uploaded May 29, 2026, after the model's April 24, 2026 release.Source: §6 · p. 9
LLM stochasticity
- Ten runs per theorem and reporting both pass@10 and trial-level success are used to reduce the effect of LLM stochasticity.The artifact includes code and run configurations for reproducing the evaluated settings.Source: §6 · p. 9
Lexical search and semantic retrieval
- Repository tools rely primarily on names, tokens, and source text, so the LLM often must guess an identifier to find a useful lemma.The authors point to semantic retrieval from proof plans, natural-language descriptions, and embeddings as a possible complement to source inspection.Source: §6 · p. 9
7 Related Work
Related work spans verified software, automated proving, theorem-proving agents, and end-to-end trusted-library generation. RAIN focuses on repository-level proof generation within that broader landscape.
7.1 Verified Software Systems
- CompCert, seL4, CertiKOS, FSCQ, and seKVM illustrate ITPs' use in substantial software verification, while their proofs still demand expertise, human effort, and time.The projects cover compiler semantics, operating-system correctness, crash-safe filesystems, and hypervisor memory protection.Source: §7.1 · p. 9
7.2 Automated Theorem Proving
- Hammers such as Sledgehammer and CoqHammer can select premises and reconstruct scripts after backend success, but induction, case analysis, repository-specific tactics, and long proof plans often remain beyond their direct reach.The section contrasts these local solvers with broader proof-engineering needs.Source: §7.2 · p. 10
- Prior systems use learned tactics, retrieval, repair, decomposition, hammers, or proof-state search; RAIN instead frames proving as an agent workflow that explores a project, edits a whole script, and revises it using enriched checker feedback.The cited work includes Rocq systems PALM [22], Rango [40], Cobblestone [17], and ReCent-Prover [35], alongside systems for other provers.Source: §7.2 · p. 10
7.3 Theorem-Proving Agents
- Lean agents demonstrate that code-agent workflows can support formal proof development; RAIN applies that direction to Rocq with repository read/write tools and enhanced checker feedback.End-to-end trusted-software work broadens the goal to producing a trusted artifact, whereas RAIN focuses on proof generation within that pipeline.Source: §7.3 · p. 10, §7.4 · p. 10
8 Conclusion
The conclusion presents repository inspection, proof editing, checker execution, and feedback-driven revision as a coding-agent workflow suited to Rocq proving. RAIN improves over prior Rocq baselines, remains competitive with coding agents at lower cost, and motivates further work on longer proofs and hybrid backends.
8 Conclusion
- RAIN combines repository inspection, proof editing, checker execution, and revision from feedback in a workflow that resembles ordinary proof engineering while keeping the checker authoritative.The conclusion presents this as a complementary approach to retrieval, repair, hammers, decomposition, and tactic-level search.Source: §8 · p. 10
- RAIN improves over prior Rocq baselines, stays competitive with strong coding agents, reduces cost, and remains effective on a recent Rocq project.The conclusion characterizes proof-specific agent design as making the workflow more effective and economical.Source: §8 · p. 10
- Future work may combine RAIN with proof decomposition for longer proofs and use cheaper specialized models for routine tasks alongside stronger LLMs for difficult repair rounds.One proposed role is using RAIN as a leaf-goal prover for generated subgoals and helper lemmas.Source: §8 · p. 10