mlsanityData to 7 Oct 2026

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

arXiv 2510.25015 ↗First posted 28 Oct 2025cs.SE cs.AIcited by 8

Not on the map. Why?

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.

Key facts. Cited by 8 papers in the map (data through 7 Oct 2026). Builds on 19 of its 42 references that are in the map. First posted on arXiv 28 Oct 2025.

Builds on

19 of 42 references.

References · 19

  1. 2020Retrieval-Augmented Generation for Knowledge-Intensive NLP Taskscited by 9,160
  2. 2022Do Users Write More Insecure Code with AI Assistants?cited by 186
  3. 2023Identifying and Mitigating the Security Risks of Generative AIcited by 90
  4. 2023Clover: Closed-Loop Verifiable Code Generationcited by 62
  5. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
  6. 2024Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verificationcited by 55
  7. 2023Verus: Verifying Rust Programs using Linear Ghost Types (extended version)cited by 50
  8. 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
  9. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  10. 2024HITS: High-coverage LLM-based Unit Test Generation via Method Slicingcited by 37
  11. 2023Finding Inductive Loop Invariants using Large Language Modelscited by 35
  12. 2024Constrained Decoding for Secure Code Generationcited by 35
7 more
  1. 2024Towards Understanding the Characteristics of Code Generation Errors Made by Large Language Modelscited by 28
  2. 2024Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languagescited by 16
  3. 2024LLM-Powered Test Case Generation for Detecting Bugs in Plausible Programscited by 14
  4. 2025ClassInvGen: Class Invariant Synthesis using Large Language Modelscited by 11
  5. 2024dafny-annotator: AI-Assisted Verification of Dafny Programscited by 8
  6. 2020Data-Driven Inference of Representation Invariantscited by 4
  7. 2024Breaking the Barrier: Enhanced Utility and Robustness in Smoothed DRL Agentscited by 4

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 1; 2026: 7.

8 papers.

  1. 2025VeruSAGE: A Study of Agent-Based Verification for Rust Systemscited by 11
  2. 2026Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agentscited by 8
  3. 2026Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Inductioncited by 2
  4. 2026VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generationcited by 1
  5. 2026Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thoughtcited by 0
  6. 2026Combining Mechanical and Agentic Specification Inference for Movecited by 0
  7. 2026An AI Approach to Verified Production Cryptographic Librariescited by 0
  8. 2026Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verificationcited by 0