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

Sicheng Zhong, Jiading Zhu, Yifang Tian +1

Scaling automated formal verification to real-world projects requires resolving cross-module dependencies and global contexts, which are challenges overlooked by existing function-…