Toward Repository-Level Program Verification with Large Language Models
summary
Introduces a repository-scale verification benchmark RVBench with ~750 proof tasks and >12,000 proof lines drawn from four real Verus projects, and a pipeline RagVerus that uses retrieval-augmented generation with per-function embeddings plus a metadata index to fetch helper functions and proof-pattern examples; RagVerus triples proof pass rates on prior benchmarks under constrained inference and yields a 27% relative improvement on RVBench, with a refinement loop that uses verifier errors to auto-repair proofs.
AI-written summary · about
chapters (11)
- 0:00Repository-level verification intro
- 1:08Formal verification importance
- 2:31Manual proof challenges
- 4:40Verification complexity
- 6:25Context retrieval with RAG-Varius
- 7:31Proof completion example
- 10:20Building search indexes
- 11:50Proof generation process
- 12:31RVBench benchmark
- 14:40Evaluation results
- 15:28Q&A
related talks
34mFrom Vibe Coding to Vericoding
16mLemur: Integrating Large Language Models in Automated Program Verification
18mLaurel: Unblocking Automated Verification with Large Language Models
21mVerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model,(…)
31mBeyond LLMs and Maturing RAG use cases
18mRISC-V Spotlight: Improving RISC-V Quality with Verification Standards and Advanc...
22mTowards Verified Code Reasoning by LLMs
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems