VerusSeek: Retrieval-Augmented LLM-Based Proof Synthesis for Rust Programs
Open Access
- 7 October 2026
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 3402-3406
Abstract
No abstract availableFunding Information
- NSFC (62472339)
This publication has 13 references indexed in Scilit:
- Enhancing LLM-Based Proof Synthesis for Rust Programs via Semantic Chunking and Hierarchical Context Expansion2026
- Towards Repository-Level Program Verification with Large Language Models2025
- AutoVerus: Automated Proof Generation for Rust CodeProceedings of the ACM on Programming Languages, 2025
- Integrating ensemble learning and Large Language Models for efficient formal verification of IP-based aerospace systemsInformation Fusion, 2025
- Verus: A Practical Foundation for Systems Verification2024
- Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification2024
- Clover: Closed-Loop Verifiable Code Generation2024
- Towards AI-Assisted Synthesis of Verified Dafny MethodsProceedings of the ACM on Software Engineering, 2024
- Diffy: Inductive Reasoning of Array Programs Using Difference Invariants2021
- RustBelt: securing the foundations of the Rust programming languageProceedings of the ACM on Programming Languages, 2017