In this paper, we describe early work on a specification inference tool for the Move Prover that combines a weakest-precondition (WP) analysis over Move bytecode with an agentic coding CLI such as Claude Code. Specification inference reduces the boilerplate of writing specifications in Move: in order to verify a high-level property such as a global state invariant, pre- and post-conditions for the supporting functions typically have to be written by hand, which is tedious. In our setting, a Model Context Protocol (MCP) service exposes the WP analysis and the prover itself to the coding agent. The WP analysis provides a sound, mechanical baseline for inference; the AI is used precisely where WP is weakest -- for loop invariants and high-level idiomatic specifications such as monotonicity, conservation, and structural invariants. The Move Prover serves as the oracle that decides whether the generated specs are valid, and the agent is equipped to generate proof hints and to refine the inferred specification until verification succeeds. The tool has been applied to a corpus of canonical Move code, including code that uses higher-order functions, dynamic dispatch, global state, references, and various forms of loops.

翻译：本文描述了为 Move Prover 开发的规格推断工具的初步工作，该工具将移动字节码上的最弱前置条件分析（WP）与诸如 Claude Code 之类的智能体编码命令行界面相结合。规格推断减少了在 Move 中编写规格的模板化工作：为验证高层性质（例如全局状态不变量），支持函数的前置条件和后置条件通常需要手动编写，这十分繁琐。在我们的方案中，模型上下文协议（MCP）服务向编码智能体暴露了 WP 分析和证明器本身。WP 分析为推断提供了可靠的、机械化的基线；人工智能被精确地应用在 WP 最薄弱的环节——即循环不变量以及高层惯用规格（例如单调性、守恒性和结构不变量）。Move Prover 充当决定生成的规格是否有效的仲裁者，并且智能体能够生成证明提示并细化推断出的规格，直到验证成功。该工具已应用于一组规范的 Move 代码，包括使用高阶函数、动态分派、全局状态、引用和各种循环形式的代码。