AI summaryⓘ
The authors explain how they improved the Move Prover (MVP), a tool that checks smart contracts written in the Move language, to handle higher-order functions—functions that can be treated like data and passed around. They introduce a way to describe these functions' behavior using special predicates that track how functions change program state. Their method efficiently encodes these functions for automated reasoning tools and supports advanced features like functions that modify state via references or global variables, which is more powerful than some existing systems. The authors also enhanced MVP’s ability to automatically infer specifications for such functions, making it easier to verify complex smart contracts.
Move ProverMove languagehigher-order functionssmart contractsbehavioral predicatesSMT encodingweakest-precondition analysisdynamic dispatchspecification inferenceformal verification
Authors
Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap, Jake Silverman
Abstract
The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language. Recently, Move on Aptos was extended with higher-order functions: imperative functions as first-class values that can be passed around, stored in data structs, and kept in persistent storage, enabling dynamic dispatch. This paper describes the representation of function values in the Move specification language and their implementation in MVP. We introduce behavioral predicates which characterize Move functions (aborts and pre/post conditions) by single-state or two-state predicates. We also introduce state labels for naming intermediate memory states in which expressions are evaluated and which allow to compose behavioral predicates to describe sequences of state transitions. On SMT level, function values are encoded by discriminating over the possible function values reaching a call site: when the concrete function is known, its effect is accounted for directly; when it is unknown (for example, a function parameter, or a closure loaded from storage), its behavioral predicates describe the effect. Our approach goes beyond, for example, Dafny, by supporting imperative first-class functions which can modify state via Rust-style references and global variables, and leads to more efficient SMT encodings than separation logic because of the static separation of memory enabled by Move. We further extend MVP's specification inference tool to work with function values: given arbitrary higher-order Move code, weakest-precondition analysis semi-automatically derives behavioral-predicate-based specifications, reducing the annotation burden and providing a validation pipeline for the new specification constructs.