VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu Lahiri, Shan Lu, David Dill, Clark Barrett
TL;DR
VeriStruct introduces an AI-assisted framework for automatically verifying Rust data-structure modules in Verus, addressing the difficulty of scaling verification beyond single functions. It combines a planner with four specialized annotation-generation modules (View, Type Invariant, Specifications, and Proof Blocks) and a repair stage to fix verifier-reported errors, thereby enabling joint verification of multiple methods under a shared invariant. In evaluation over eleven benchmarks totaling $129$ functions, VeriStruct verifies $128$ functions across $11$ benchmarks (i.e., $99.2\%$) and solves $10$ of $11$ benchmarks, outperforming a baseline whose single-shot LLM approach verifies far fewer functions. The work demonstrates a practical path toward AI-assisted formal verification at scale and outlines concrete directions (RAG, concurrency libraries, constrained decoding, and automatic unit-test generation) to further enhance automation and reliability.
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.