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

Abstract: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.

In Proceedings FROM 2026, arXiv:2609.30324

Artificial Intelligence (cs.AI); Programming Languages (cs.PL); Software Engineering (cs.SE)

arXiv:2609.34886 [cs.AI]

(or arXiv:2609.34886v1 [cs.AI] for this version)

https://doi.org/10.48550/arXiv.2609.34886 Focus to learn more arXiv-issued DOI via DataCite (pending registration)

EPTCS 452, 2026, pp. 104-121

https://doi.org/10.4204/EPTCS.452.8 Focus to learn more DOI(s) linking to related resources

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.