一句话：提出 Msg，面向 Move 智能合约自动生成可验证规约，84% 函数成功，可验证子句提升 57%。
基于 LLM 的规约生成已开始受到关注，但现有工具主要面向 C、Java 甚至 Solidity 等主流语言，对 Move 这类新兴且以验证为导向的语言尚缺探索。本文提出 Msg，一个面向 Move 智能合约的自动化规约生成工具，旨在揭示将 LLM 规约生成迁移到新生态时出现的独特洞见。Msg 表明 LLM 对非主流语言同样具备稳健的代码理解与生成能力：它为 84% 的受测 Move 函数成功生成可验证规约，甚至识别出专家此前忽略的子句。此外，Msg 通过智能体式、模块化的设计显式利用规约语言特性，显著提升规约质量，相比传统设计多生成 57% 的可验证子句；引入验证工具链反馈后，可验证规约数量进一步增加 30%。
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.
DOI 原文 ·
@inproceedings{paperbot9505,
title = {Agentic Specification Generator for Move Programs},
author = {Yu-Fu Fu and Meng Xu and Taesoo Kim},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00110}
}