![[2510.25015] VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus](https://arxiv.org/static/browse/0.3.4/images/arxiv-logo-fb.png){kind=logo}
[2510.25015] VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Summary
VeriStruct is a novel framework for AI-assisted automated verification of complex data structure modules in Verus, achieving a high success rate in verification tasks.
Why It Matters
This research addresses the challenges of verifying complex data structures, which is crucial for ensuring software reliability. By improving AI-assisted verification methods, it contributes to advancements in software engineering and formal verification, potentially impacting various applications in AI and software development.
Key Takeaways
- VeriStruct extends AI-assisted verification to complex data structures.
- The framework achieved a 99.2% success rate in verifying functions.
- It incorporates syntax guidance and a repair stage for annotation errors.
- This work represents a significant step toward automatic formal verification.
- The results can enhance reliability in software engineering practices.
Computer Science > Software Engineering arXiv:2510.25015 (cs) [Submitted on 28 Oct 2025 (v1), last revised 18 Feb 2026 (this version, v3)] Title:VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus Authors:Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu Lahiri, Shan Lu, David Dill, Clark Barrett View a PDF of the paper titled VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus, by Chuyue Sun and 7 other authors View PDF HTML (experimental) Abstract:We introduce VeriStruct, a novel framework that extends AI-assisted automated verification from single functions to more complex data structure modules in Verus. VeriStruct employs a planner module to orchestrate the systematic generation of abstractions, type invariants, specifications, and proof code. To address the challenge that LLMs often misunderstand Verus' annotation syntax and verification-specific semantics, VeriStruct embeds syntax guidance within prompts and includes a repair stage to automatically correct annotation errors. In an evaluation on eleven Rust data structure modules, VeriStruct succeeds on ten of the eleven, successfully verifying 128 out of 129 functions (99.2%) in total. These results represent an important step toward the goal of automatic AI-assisted formal verification. Subjects: Software Engineering (cs.SE); Artificial Intelligence (cs.AI) Cite as: arXiv:2510.25015 [cs.SE] (or arXiv:2510.25015v3 [cs.SE] for this version)...