Pith. sign in

REVIEW 5 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

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 · ORCID
classification cs.SEcs.AIcs.FL
keywords proofautoveruscodegenerationrustverificationautomaticallybenchmarks
verification ladder T0 review T1 audit T2 compute T3 formal
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). Continue with ORCID to comment.

Forward citations

Cited by 5 Pith papers

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

  1. An AI Approach to Verified Production Cryptographic Libraries

    cs.CR 2026-08 conditional novelty 6.0 of 10

    An AI agent, guarded by mechanical integrity gates, synthesized Verus-verified internal specifications and proofs for curve25519-dalek and chacha20 without changing executable code.

  2. HarnessLLM: Rust Verification Harness Generation with Large Language Models

    cs.SE 2026-07 conditional novelty 6.0 of 10

    HarnessLLM extracts API calling scenarios from Rust tests and uses LLMs to synthesize Kani harnesses, achieving 100% compile success and finding 6 real memory-safety bugs.

  3. Locus: Agentic Predicate Synthesis for Directed Fuzzing

    cs.CR 2025-08 conditional novelty 6.0 of 10

    Locus uses an LLM agent to synthesize and validate intermediate predicates that make directed fuzzing reach target bug states faster, reporting an average 41.6x speedup across eight fuzzers.

  4. Proving the Coding Interview: A Benchmark for Formally Verified Code Generation

    cs.SE 2025-02 conditional novelty 6.0 of 10

    FVAPPS converts 4,715 APPS coding puzzles into Lean 4 'prove your program correct' tasks and reports that frontier LLMs prove roughly 30% of sampled theorems.

  5. RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation

    cs.SE 2025-02 conditional novelty 6.0 of 10

    Retrieval-augmented prompting improves LLM proof-completion pass rates by 27% relative on a new repository-level Verus benchmark and triples them on a function-level benchmark at low sampling budgets.

Pith tools