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开发的一款规范推断工具的早期工作，该工具将Move字节码上的最弱前置条件（WP）分析与Claude Code等智能体编码CLI相结合。规范推断减少了在Move中编写规范的工作量：为了验证诸如全局状态不变性之类的高层性质，支持函数的前置条件与后置条件通常需要手动编写，这是一项繁琐的任务。在我们的方案中，模型上下文协议（MCP）服务将WP分析和验证器本身暴露给编码智能体。WP分析为推断提供了可靠且机械性的基线；人工智能被精确地应用于WP最薄弱的环节——循环不变量以及单调性、守恒性和结构不变性等高层惯用规范。Move Prover作为裁决已生成规范是否有效的逻辑判定器，而智能体则具备生成证明提示并细化推断规范的能力，直至验证成功。该工具已应用于一组经典的Move代码，包括使用高阶函数、动态调度、全局状态、引用及各类循环的代码。