Agentic Specification Generator for Move Programs （运动程序的主体规范生成器）

于红博

摘要: 尽管基于LLM的规范生成正在受到关注，现有工具主要集中在像C、Java甚至Solidity这样的主流编程语言上，而对于新兴且面向验证的语言如Move，却鲜有探索。本文介绍了MSG，一个专为Move智能合约设计的自动化规范生成工具。MSG旨在突显将基于LLM的规范生成应用于新生态时独特的见解。具体来说，MSG表明LLMs在非主流语言中展现出了强大的代码理解和生成能力。MSG成功为测试的84%的Move函数生成可验证的规范，甚至发现了专家之前忽略的条款。此外，MSG表明通过代理化、模块化设计明确利用规范语言特性可以大幅提高规范质量（比传统设计生成了57%更多的可验证条款）。结合来自验证工具链的反馈进一步增强了MSG的效果，导致生成可验证规范的增加了30%。

更新时间: 2025-09-29 09:34:31

领域: cs.SE,cs.AI,cs.CR,cs.PL

下载: http://arxiv.org/abs/2509.24515v1