# Combining Mechanical and Agentic Specification Inference for Move

arXiv: https://arxiv.org/abs/2605.10005 · HTML: https://mlsanity.com/paper/2605.10005/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 9 of its 22 references that are in the map.
- First posted on arXiv 11 May 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 9 of 9)

- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation](https://mlsanity.com/paper/2405.02580/) (2024)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [DafnyPro: LLM-Assisted Automated Verification for Dafny Programs](https://mlsanity.com/paper/2601.05385/) (2026)
- [VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus](https://mlsanity.com/paper/2510.25015/) (2025)
- [Aeneas: Rust Verification by Functional Translation](https://mlsanity.com/paper/2206.07185/) (2022)
- [Fast and Reliable Formal Verification of Smart Contracts with the Move Prover](https://mlsanity.com/paper/2110.08362/) (2021)
- [Agentic Specification Generator for Move Programs](https://mlsanity.com/paper/2509.24515/) (2025)
- [Resources: A Safe Language Abstraction for Money](https://mlsanity.com/paper/2004.05106/) (2020)

## Abstract (arXiv)

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.