“VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus” by Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu K. Lahiri, Shan Lu, David L. Dill, and Clark W. Barrett. In Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part II, (Sebastian Junges and Guy Katz, eds.), Apr. 2026, pp. 109-128.
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.
BibTeX entry:
@inproceedings{SSA+26,
author = {Chuyue Sun and Yican Sun and Daneshvar Amrollahi and Ethan
Zhang and Shuvendu K. Lahiri and Shan Lu and David L. Dill and
Clark W. Barrett},
editor = {Sebastian Junges and Guy Katz},
title = {VeriStruct: AI-assisted Automated Verification of
Data-Structure Modules in Verus},
booktitle = {Tools and Algorithms for the Construction and Analysis of
Systems - 32nd International Conference, {TACAS} 2026, Held as
Part of the International Joint Conferences on Theory and Practice
of Software, {ETAPS} 2026, Turin, Italy, April 11-16, 2026,
Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
pages = {109--128},
publisher = {Springer},
month = apr,
year = {2026},
doi = {10.1007/978-3-032-22749-2_6},
url = {http://theory.stanford.edu/~barrett/pubs/SSA+26.pdf}
}
(This webpage was created with bibtex2web.)