Verification skill reduces assumptions for linked list correctness proofs

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

Artificial IntelligenceProgramming LanguagesSoftware Engineering

Summary

Verifying that complex computer programs work correctly can be very difficult, especially for structures like doubly linked lists, which have two-way connections and are tricky to check. The authors studied whether large language models (LLMs) can help create strong technical descriptions (specifications) for these lists without relying on unproven assumptions that might make the verification unreliable. They created a special skill for an LLM that includes expert knowledge and a way to break down the task, allowing the model to produce trustworthy specifications for doubly linked lists in the Verus verification tool. This approach helps make the program verification process less tedious and more reliable.

What this means in practice

Authors

Andrada-Livia Antoneac, Dorel Lucanu, Dragoş Teodor Gavriluţ

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.
View PDFOpen arXiv