arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2610.30759

RAIN: Agentic Proof Generation for Rocq-based Software Verification

Jinyi Zhou·Zenan Li·Yuan Yao·Jun Ma·Taolue Chen·Xiaoxing Ma
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Jinyi Zhou, Zenan Li, Yuan Yao, Jun Ma, Taolue Chen, Xiaoxing Ma. 2026-10-22. RAIN: Agentic Proof Generation for Rocq-based Software Verification. https://arxiv.org/abs/2610.30759

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A declarative approach to specifying Paxos using three-valued modal fixpoint logic

We present Three-valued Fixpoint Quorum Logic, or 3muQL for short; a three-valued modal fixed-point logic designed for declaratively specifying and reasoning about distributed algorithms, such as the Paxos consensus algorithm. Our methodology represents a distributed algorithm as a logical theory, enabling correctness properties to be derived directly within the framework -- or revealing logical errors in the algorithm's design when they exist. 3muQL adopts a declarative approach, specifying the overall logic of computation without prescribing control flow. Notably, message-passing and state-transitions are not explicitly modelled, and notions of 'quorum' are abstracted from concrete thresholds to abstract modal operators. This distinguishes our framework from approaches like TLA+. The logical abstraction emphasises the essence of distributed algorithms, offering a novel perspective on their specification and reasoning. We define the syntax and semantics of 3muQL, explore its theoretical properties, and demonstrate its applicability through a detailed treatment of the Paxos consensus algorithm. By presenting Paxos as a logical theory and deriving its standard correctness properties, we showcase the framework's capacity to handle non-trivial distributed systems. We envision 3muQL as a versatile tool for specifying and reasoning about distributed algorithms. The Paxos example highlights the framework's ability to capture intricate details, offering a new lens through which distributed algorithms can be specified, studied, and checked. The ideas we present are easily implemented, and to demonstrate this we have implemented a freely-available proof-of- concept 3muQL model-checker, as an effective prototyping tool.

cs.LO↗
arXiv2026

Ohana trees, linear approximation and multi-types for the $λ$I-calculus: No variable gets left behind or forgotten!

Although the $λ$I-calculus is a natural fragment of the $λ$-calculus, obtained by forbidding the erasure of arguments, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable $λ$I-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the $λ$I-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a $λ$I-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. We develop the associated theories of program approximation: the first approach -- more classic -- is based on finite trees and continuity, the second adapts Ehrhard and Regnier's Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a $λ$I-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. Subsequently, we introduce a denotational model designed to capture the equality induced by Ohana trees. Although presented as a non-idempotent type system, our model is based on a suitably modified version of the relational semantics of the $λ$-calculus, which is known to yield proper models of the $λ$I-calculus when restricted to non-empty finite multisets. To track variables occurring in subterms that are hidden or pushed to infinity in the evaluation trees, we generalize the system in two ways: first, we reintroduce annotated versions of the empty multiset indexed by sets of variables; second, (...)

cs.LO↗
arXiv2026

A simple formalization of alpha-equivalence

While teaching untyped $λ$-calculus to undergraduate students, we were wondering why $α$-equivalence is not directly inductively defined. In this paper, we demonstrate that this is indeed feasible. Specifically, we provide a grounded, inductive definition for $α$-equivalence and show that it conforms to the specification provided in the literature. The work presented in this paper is fully formalized in the Rocq Prover.

cs.LO↗