# VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

arXiv: https://arxiv.org/abs/2510.25015 · HTML: https://mlsanity.com/paper/2510.25015/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 42 references that are in the map.
- First posted on arXiv 28 Oct 2025.

## Builds on (most cited first, 19 of 19)

- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Do Users Write More Insecure Code with AI Assistants?](https://mlsanity.com/paper/2211.03622/) (2022)
- [Identifying and Mitigating the Security Risks of Generative AI](https://mlsanity.com/paper/2308.14840/) (2023)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [HITS: High-coverage LLM-based Unit Test Generation via Method Slicing](https://mlsanity.com/paper/2408.11324/) (2024)
- [Constrained Decoding for Secure Code Generation](https://mlsanity.com/paper/2405.00218/) (2024)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [Towards Understanding the Characteristics of Code Generation Errors Made by Large Language Models](https://mlsanity.com/paper/2406.08731/) (2024)
- [Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages](https://mlsanity.com/paper/2406.09757/) (2024)
- [LLM-Powered Test Case Generation for Detecting Bugs in Plausible Programs](https://mlsanity.com/paper/2404.10304/) (2024)
- [ClassInvGen: Class Invariant Synthesis using Large Language Models](https://mlsanity.com/paper/2502.18917/) (2025)
- [dafny-annotator: AI-Assisted Verification of Dafny Programs](https://mlsanity.com/paper/2411.15143/) (2024)
- [Data-Driven Inference of Representation Invariants](https://mlsanity.com/paper/2003.12106/) (2020)
- [Breaking the Barrier: Enhanced Utility and Robustness in Smoothed DRL Agents](https://mlsanity.com/paper/2406.18062/) (2024)

## Built on by (most cited first, 9 of 9)

- [VeruSAGE: A Study of Agent-Based Verification for Rust Systems](https://mlsanity.com/paper/2512.18436/) (2025)
- [Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents](https://mlsanity.com/paper/2603.17150/) (2026)
- [VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation](https://mlsanity.com/paper/2605.08553/) (2026)
- [Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction](https://mlsanity.com/paper/2602.04892/) (2026)
- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought](https://mlsanity.com/paper/2603.18334/) (2026)
- [Combining Mechanical and Agentic Specification Inference for Move](https://mlsanity.com/paper/2605.10005/) (2026)
- [An AI Approach to Verified Production Cryptographic Libraries](https://mlsanity.com/paper/2608.00965/) (2026)
- [Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification](https://mlsanity.com/paper/2609.34886/) (2026)

## Abstract (arXiv)

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.