设计更少的假设：LLM 辅助 Verus 验证的可重用技能

LLM 辅助的 Verus 验证是验证 Rust 实现的一种不太繁琐的方法，但与自引用结构（例如双向链表（DLL））配合使用——众所周知，很难形式化验证——它变成了一项要求更高的验证任务。此外，当验证依赖于未经证实或无效的假设（例如公理引理和假设陈述）时，可能会出现规范弱点。我们研究 LLM Agent是否可以合成强大的 DLL 规范，同时最小化这些可信基础。该分析遵循三种不同的方法：手动验证、特定于属性的验证以及针对 DLL 的特定情况和此类数据结构的某些属性的定义技能。该技能编码领域知识和任务分解策略。我们证明，配备精心设计的验证技能的 LLM Agent可以为 Verus 中的 DLL 生成强大的、低信任度的规范。