VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910039473651712 |
|---|---|
| author | Sun, Chuyue Sun, Yican Amrollahi, Daneshvar Zhang, Ethan Lahiri, Shuvendu Lu, Shan Dill, David Barrett, Clark |
| author_facet | Sun, Chuyue Sun, Yican Amrollahi, Daneshvar Zhang, Ethan Lahiri, Shuvendu Lu, Shan Dill, David Barrett, Clark |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_25015 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus Sun, Chuyue Sun, Yican Amrollahi, Daneshvar Zhang, Ethan Lahiri, Shuvendu Lu, Shan Dill, David Barrett, Clark Software Engineering Artificial Intelligence 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. |
| title | VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus |
| topic | Software Engineering Artificial Intelligence |
| url | https://arxiv.org/abs/2510.25015 |