Combining Mechanical and Agentic Specification Inference for Move

TL;DR

This paper presents a tool that combines weakest-precondition analysis with AI-based inference to automate and improve the specification process for Move programs, reducing manual effort.

Contribution

It introduces a novel approach that integrates mechanical WP analysis with agentic AI to infer specifications, especially for complex high-level properties in Move code.

Findings

The tool successfully infers specifications for complex Move code including higher-order functions and global state.

AI refinement improves the accuracy of inferred specifications until verification succeeds.

The approach reduces manual effort in writing Move specifications by automating inference.

Abstract

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.