# Agentic Specification Generator for Move Programs

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 18 of its 62 references that are in the map.
- First posted on arXiv 29 Sep 2025.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

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

- [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023)
- [Repository-Level Prompt Generation for Large Language Models of Code](https://mlsanity.com/paper/2206.12839/) (2022)
- [GPTScan: Detecting Logic Vulnerabilities in Smart Contracts by Combining GPT with Program Analysis](https://mlsanity.com/paper/2308.03314/) (2023)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [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)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages](https://mlsanity.com/paper/2406.09757/) (2024)
- [How Effective are Large Language Models in Generating Software Specifications?](https://mlsanity.com/paper/2306.03324/) (2023)
- [OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification](https://mlsanity.com/paper/2504.20964/) (2025)
- [Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models](https://mlsanity.com/paper/2412.10483/) (2024)
- [solc-verify: A Modular Verifier for Solidity Smart Contracts](https://mlsanity.com/paper/1907.04262/) (2019)
- [Fast and Reliable Formal Verification of Smart Contracts with the Move Prover](https://mlsanity.com/paper/2110.08362/) (2021)
- [A Survey of Practical Formal Methods for Security](https://mlsanity.com/paper/2109.01362/) (2021)
- [Formal Methods in Railways: a Systematic Mapping Study](https://mlsanity.com/paper/2107.05413/) (2021)

## Built on by (most cited first, 3 of 3)

- [Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization](https://mlsanity.com/paper/2605.26457/) (2026)
- [Reproducible, Explainable, and Effective Evaluations of Agentic AI for Software Engineering](https://mlsanity.com/paper/2604.01437/) (2026)
- [Combining Mechanical and Agentic Specification Inference for Move](https://mlsanity.com/paper/2605.10005/) (2026)

## Abstract (arXiv)

While LLM-based specification generation is gaining traction, existing tools primarily focus on mainstream programming languages like C, Java, and even Solidity, leaving emerging and yet verification-oriented languages like Move underexplored. In this paper, we introduce MSG, an automated specification generation tool designed for Move smart contracts. MSG aims to highlight key insights that uniquely present when applying LLM-based specification generation to a new ecosystem. Specifically, MSG demonstrates that LLMs exhibit robust code comprehension and generation capabilities even for non-mainstream languages. MSG successfully generates verifiable specifications for 84% of tested Move functions and even identifies clauses previously overlooked by experts. Additionally, MSG shows that explicitly leveraging specification language features through an agentic, modular design improves specification quality substantially (generating 57% more verifiable clauses than conventional designs). Incorporating feedback from the verification toolchain further enhances the effectiveness of MSG, leading to a 30% increase in generated verifiable specifications.