Pith. sign in

REVIEW 4 cited by

AutoVerus: Automated Proof Generation for Rust Code

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2409.13082 v3 pith:KEUQILQK submitted 2024-09-19 cs.SE cs.AIcs.FL

AutoVerus: Automated Proof Generation for Rust Code

Chenyuan Yang , Xuheng Li , Md Rakib Hossain Misu , Jianan Yao , Weidong Cui , Yeyun Gong , Chris Hawblitzel , Shuvendu Lahiri
show 5 more authors
Jacob R. Lorch Shuai Lu Fan Yang Ziqiao Zhou Shan Lu
This is my paper
classification cs.SE cs.AIcs.FL
keywords proofautoveruscodegenerationrustverificationautomaticallybenchmarks
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved
0 comments
read the original abstract

Generative AI has shown its values 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 LLM 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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 4 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. FVSpec: Real-World Property-Based Tests as Lean Challenges

    cs.SE 2026-05 conditional novelty 7.0

    A new benchmark of 9,415 Lean 4 specifications derived from 2,772 scraped Python property-based tests, plus a three-agent LLM transpilation pipeline and proof-generation baselines.

  2. Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems

    cs.AI 2026-05 unverdicted novelty 7.0

    IDS is an agentic LLM system that incrementally synthesizes both implementation and proof for distributed key-value stores, succeeding on all 7 specs where prior agents succeeded on only 2.

  3. AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

    cs.SE 2026-05 unverdicted novelty 6.0

    AutoSOUP automates component-level memory-safety verification by generating Safety-Oriented Unit Proofs via three techniques and a hybrid LLM-plus-program-synthesis architecture called LLM-As-Function-Call.

  4. Automating Formal Verification with Reinforcement Learning and Recursive Inference

    cs.LG 2026-05 unverdicted novelty 5.0

    RLVR training raises verified Dafny pass rates from 9.7% to 31.1% on a filtered benchmark while a Lean proof scaffold lifts success from 46.2% to 69.2% on a pilot set and solves 7 of 42 prior unsolved tasks.