通过设计减少假设：面向LLM辅助Verus验证的可复用技能
Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification
浏览论文内容
中文总结 AI 辅助
本研究探索LLM代理在Verus中为双向链表生成强规范，通过设计可复用技能减少假设，实现低信任验证。
中文摘要 AI 辅助
LLM辅助的Verus验证是一种减少繁琐性的方法来验证Rust实现，但当与自引用结构（例如双向链表（DLLs）——众所周知难以形式化以进行验证）结合时，它变成了一项要求高得多的验证任务。此外，当验证依赖于未经证明或无效的假设（如公理引理和assume语句）时，可能会出现规范弱点。我们研究LLM代理是否能在最小化这些可信基础的同时综合出强DLL规范。分析遵循三种不同的方法：手动验证、属性特定验证，以及针对DLLs特定情况和此类数据结构某些属性的定义技能。该技能编码了领域知识和任务分解策略。我们表明，配备精心设计的验证技能的LLM代理可以在Verus中为DLLs生成强健、低信任的规范。
英文摘要
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.
发表机构
- Bitdefender（比特梵德）
- Alexandru Ioan Cuza University of Iași（雅西亚历山德鲁·伊万·库扎大学）
机构由 AI 辅助整理，请以论文原文为准。
