Combining Mechanical and Agentic Specification Inference for Move
2026-05-11 • Programming Languages
Programming LanguagesArtificial IntelligenceLogic in Computer ScienceSoftware Engineering
AI summaryⓘ
The authors developed an early tool that helps automatically create formal specifications for programs written in the Move language, which is usually a tedious task. Their tool combines a traditional program analysis technique called weakest-precondition analysis with an AI coding assistant to guess missing parts like loop invariants and high-level properties. The AI proposes these guesses, and the Move Prover checks if they’re correct, refining them as needed until verification passes. They tested the tool on various typical Move programs involving complex features like loops and global state.
Move Proverweakest-precondition analysisspecification inferenceloop invariantsAI coding assistantformal verificationglobal statepost-conditionsproof hintsdynamic dispatch
Authors
Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap
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.