# Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 17 references that are in the map.
- First posted on arXiv 28 Sep 2026.

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

- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [CBMC: The C Bounded Model Checker](https://mlsanity.com/paper/2302.02384/) (2023)
- [VeruSAGE: A Study of Agent-Based Verification for Rust Systems](https://mlsanity.com/paper/2512.18436/) (2025)
- [DafnyPro: LLM-Assisted Automated Verification for Dafny Programs](https://mlsanity.com/paper/2601.05385/) (2026)
- [VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus](https://mlsanity.com/paper/2510.25015/) (2025)
- [Aeneas: Rust Verification by Functional Translation](https://mlsanity.com/paper/2206.07185/) (2022)

## Abstract (arXiv)

LLM-assisted Verus verification is a less tedious method to verify Rust implementations, but paired with self-referential structures, e.g., Doubly Linked Lists (DLLs)—notoriously difficult to formalise for verification—it becomes a substantially more demanding verification task. Moreover, a specification weakness can arise when verification relies on unproven or invalidated assumptions, such as axiomatic lemmas and assume statements. We investigate whether LLM agents can synthesize strong DLL specifications while minimizing these trusted base. The analysis follows three different approaches: manual verification, property-specific verification, and a defined skill for the specific case of DLLs and certain properties of this type of data structure. The skill encodes domain knowledge and a task-decomposition strategy. We show that an LLM agent equipped with a carefully designed verification skill can generate strong, low-trust specifications for DLLs in Verus.