AUTOVERUS: Automated Proof Generation for Rust Code

doi:10.1145/3763174

AUTOVERUS: Automated Proof Generation for Rust Code

2025-10-01

0

PRE

AI

Md Rakib Hossain Misu

DOI：10.1145/3763174

Original request for help

Save

Abstract

En 中文

Generative AI has shown its value for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generation. In this paper, we present AUTOVERUS. AUTOVERUS uses LLMs to automatically generate correctness proof for Rust code. AUTOVERUS is designed to match the unique features of Verus, a verification tool that can prove the correctness of Rust code using proofs and specifications also written in Rust. AUTOVERUS consists of a network of agents that are crafted and orchestrated to mimic human experts' three phases of proof construction: preliminary proof generation, proof refinement guided by generic tips, and proof debugging guided by verification errors. To thoroughly evaluate AUTOVERUS and help foster future research in this direction, we have built a benchmark suite of 150 non-trivial proof tasks, based on existing code-generation benchmarks and verification benchmarks. Our evaluation shows that AUTOVERUS can automatically generate correct proof for more than 90% of them, with more than half of them tackled in less than 30 seconds or 3 LLM calls.

Keywords:

Program Verification

Program Synthesis

Verus

Large Language Models

AUTOVERUS: Automated Proof Generation for Rust Code

Abstract

Journal

Organization