Combining Mechanical and Agentic Specification Inference for Move

arXiv:2605.10005v1 Announce Type: cross 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...