用AI+机械分析自动生成Move语言验证规范，省去手动编写繁琐代码。
Combining Mechanical and Agentic Specification Inference for Move
- 结合最弱前提分析与AI编码代理，自动推导函数规约。
- 在真实Move代码上验证成功，支持高阶函数和动态分发等复杂特性。
- 特别擅长推断循环不变量等人类难写的高阶规范，适合形式化验证开发者。
本文介绍Move Prover中一种规范推断工具的早期工作，该工具结合了对Move字节码的最弱前提（WP）分析与基于AI的编码命令行接口（如Claude Code）。规范推断可减少在Move中编写规格说明的重复劳动：为验证全局状态不变性等高层性质，通常需手工撰写支持函数的前置和后置条件，过程繁琐。本方法中，模型上下文协议（MCP）服务将WP分析和验证器暴露给编码代理。WP分析提供可靠的机械基线推断；而当WP能力不足时（如循环不变量、单调性、守恒性等高阶语义），则由AI负责推断。验证器作为判定依据，指导代理生成证明提示并迭代优化推测出的规范，直至验证通过。该工具已在包含高阶函数、动态分发、全局状态、引用及多种循环结构的典型Move代码库上应用。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。