用智能体生成Move语言合约的可验证规范，效果超传统方法。
Agentic Specification Generator for Move Programs
- 设计智能体模块化系统，显式利用规范语言特性提升生成质量。
- 对84%的Move函数生成可验证规范，比常规方法多出57%有效条款。
- 结合验证工具反馈迭代，使可验证规范数量提升30%。
尽管基于大模型的规格生成逐渐流行，现有工具主要集中于C、Java等主流语言，对新兴且注重验证的Move语言关注不足。本文提出MSG，一种专为Move智能合约设计的自动化规格生成工具。实验表明，大模型在非主流语言上仍具备强代码理解与生成能力。MSG成功为84%的测试函数生成可验证规格，并发现专家遗漏的关键条款。通过智能体的模块化设计显式利用规格语言特征，生成的可验证条款比传统方法多57%。进一步融合验证工具链反馈，使可验证规格数量提升30%。
原文摘要 · Abstract (English)
While LLM-based specification generation is gaining traction, existing tools primarily focus on mainstream programming languages like C, Java, and even Solidity, leaving emerging and yet verification-oriented languages like Move underexplored. In this paper, we introduce MSG, an automated specification generation tool designed for Move smart contracts. MSG aims to highlight key insights that uniquely present when applying LLM-based specification generation to a new ecosystem. Specifically, MSG demonstrates that LLMs exhibit robust code comprehension and generation capabilities even for non-mainstream languages. MSG successfully generates verifiable specifications for 84% of tested Move functions and even identifies clauses previously overlooked by experts. Additionally, MSG shows that explicitly leveraging specification language features through an agentic, modular design improves specification quality substantially (generating 57% more verifiable clauses than conventional designs). Incorporating feedback from the verification toolchain further enhances the effectiveness of MSG, leading to a 30% increase in generated verifiable specifications.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。