Formal Verification of Imperative First-Class Functions in Move

• URL: http://arxiv.org/abs/2605.10007v2
• Date: Wed, 13 May 2026 02:34:36 GMT
• Title: Formal Verification of Imperative First-Class Functions in Move
• Abstract summary: Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language.<n>This paper describes the representation of function values in the Move specification language and their implementation in MVP.
• Score: 2.6265820258267794
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Rethinking Item Tokenization in Generative Recommenders: From Fixed Atoms to Semantic Subwords [50.621722853036005]
  In generative recommender systems, items are typically tokenized into fixed-length semantic ID sequences for autoregressive next-item prediction.<n>For user-context modeling, this fine-grained representation triggers Intra-item Attention Overload.<n>We propose Semantic Subword Tokenization (SST), which represents historical items as variable-length semantic subwords.
  arXiv  Detail & Related papers  (2026-08-24T02:42:51Z)
• Human Label Variation as Stable Signal: Learning Annotator-Specific Explanation Behavior via Cross-Annotator Preference Optimization [51.93456979139756]
  Free-text explanations extend human label variation beyond label disagreement.<n>We study whether large language models can learn and reproduce such annotator-specific label-explanation behavior.
  arXiv  Detail & Related papers  (2026-05-27T17:55:00Z)
• From Abstraction to Instantiation: Learning Behavioral Representation for Vision-Language-Action Model [76.88595728131288]
  Vision-Language-Action (VLA) models often suffer from performance degradation under distribution shifts.<n>We propose textbfBehaviorVLA, a framework that facilitates robust manipulation through the learning of a temporally coherent behavioral representations.<n> Experiments on RoboTwin 2.0, LIBERO, and CALVIN demonstrate state-of-the-art success rates of 58%, 98%, and 4.36 (Avg.Len)
  arXiv  Detail & Related papers  (2026-05-21T16:14:19Z)
• Combining Mechanical and Agentic Specification Inference for Move [2.8693521708495684]
  We describe a specification inference tool for the Move Prover.<n>It combines a weakest-precondition analysis over Move bytecode with an agentic coding CLI such as Claude Code.<n>The tool has been applied to a corpus of canonical Move code.
  arXiv  Detail & Related papers  (2026-05-11T05:30:25Z)
• GUIDED: Granular Understanding via Identification, Detection, and Discrimination for Fine-Grained Open-Vocabulary Object Detection [54.19989440021701]
  Fine-grained open-vocabulary object detection (FG-OVD) aims to detect novel object categories described by attribute-rich texts.<n>FG-OVD achieves new state-of-the-art results, demonstrating the benefits of disentangled modeling and modular optimization.
  arXiv  Detail & Related papers  (2026-03-27T22:08:11Z)
• Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications [2.5164739639003364]
  We extend mining procedures to operate over richer datatypes.<n>We demonstrate our approach reactive programs from mined specifications on the OpenAI-Gymnasium ToyText environments.
  arXiv  Detail & Related papers  (2026-03-05T19:56:25Z)
• Mechanistic Knobs in LLMs: Retrieving and Steering High-Order Semantic Features via Sparse Autoencoders [8.188989044347595]
  We propose a Sparse Autoencoder-based framework for retrieving and steering semantically interpretable internal features.<n>Using the Big Five personality traits as a case study, we demonstrate that our method enables precise, bidirectional steering of model behavior.
  arXiv  Detail & Related papers  (2026-01-06T12:40:37Z)
• Text2Mem: A Unified Memory Operation Language for Memory Operating System [59.082901444153684]
  We introduce Text2Mem, a unified memory operation language for model agents.<n>Text2Mem provides a standardized pathway from natural correctness reliable execution.
  arXiv  Detail & Related papers  (2025-09-14T07:30:09Z)
• IMoRe: Implicit Program-Guided Reasoning for Human Motion Q&A [25.91990824698619]
  We propose an implicit program-guided motion reasoning (IMoRe) framework that unifies reasoning across multiple query types without manually designed modules.<n>We introduce a program-guided reading mechanism, which dynamically selects multi-level motion representations from a pretrained motion Vision Transformer (ViT)<n>Our model achieves state-of-the-art performance on Babel-QA and generalizes to a newly constructed motion Q&A dataset based on HuMMan.
  arXiv  Detail & Related papers  (2025-08-04T01:44:41Z)
• FIND: A Function Description Benchmark for Evaluating Interpretability Methods [86.80718559904854]
  This paper introduces FIND (Function INterpretation and Description), a benchmark suite for evaluating automated interpretability methods. FIND contains functions that resemble components of trained neural networks, and accompanying descriptions of the kind we seek to generate. We evaluate methods that use pretrained language models to produce descriptions of function behavior in natural language and code.
  arXiv  Detail & Related papers  (2023-09-07T17:47:26Z)
• First-Order Stable Model Semantics with Intensional Functions [2.1955512452222696]
  We extend the first-order stable model semantics by Ferraris, Lee, and Lifschitz to allow intensional functions. We use this extension as a basis for defining Answer Set Programming Modulo Theories (ASPMT) ASPMT can be applied to domains containing real numbers and alleviates the grounding problem.
  arXiv  Detail & Related papers  (2023-07-15T06:03:35Z)
• Graph Adaptive Semantic Transfer for Cross-domain Sentiment Classification [68.06496970320595]
  Cross-domain sentiment classification (CDSC) aims to use the transferable semantics learned from the source domain to predict the sentiment of reviews in the unlabeled target domain. We present Graph Adaptive Semantic Transfer (GAST) model, an adaptive syntactic graph embedding method that is able to learn domain-invariant semantics from both word sequences and syntactic graphs.
  arXiv  Detail & Related papers  (2022-05-18T07:47:01Z)
• Parameter-Efficient Tuning by Manipulating Hidden States of Pretrained Language Models For Classification Tasks [49.807185872741066]
  We propose a simple tuning method which only introduces three trainable vectors. We input the integrated hidden state(s) to a task-specific linear classifier to predict categories. This scheme is similar to the way ELMo utilises hidden states except that they feed the hidden states to LSTM-based models.
  arXiv  Detail & Related papers  (2022-04-10T04:14:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.