arxiv: 2605.10007 · v2 · submitted 2026-05-11 · 💻 cs.PL · cs.LO· cs.SE

Recognition: no theorem link

Formal Verification of Imperative First-Class Functions in Move

Wolfgang Grieskamp , Teng Zhang , Vineeth Kashyap , Jake Silverman

Authors on Pith no claims yet

Pith reviewed 2026-05-14 21:57 UTC · model grok-4.3

classification 💻 cs.PL cs.LOcs.SE

keywords formal verificationMove languagefirst-class functionsbehavioral predicatesSMT encodingsmart contractshigher-order functionsstate labels

0 comments

The pith

The Move Prover verifies imperative first-class functions by encoding their state effects with behavioral predicates and state labels.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to extend the Move Prover to handle higher-order imperative functions that can be passed, stored, and called to modify global state or references. It represents these functions with behavioral predicates that capture abort conditions and pre/post states as single-state or two-state predicates. State labels name intermediate memory states so predicates can be composed into sequences of transitions. At the SMT level the encoding discriminates at each call site: known functions contribute their direct effects while unknown ones, such as parameters or storage-loaded closures, are summarized by their predicates. The same machinery extends the prover's weakest-precondition inference so that specifications for arbitrary higher-order Move code can be derived automatically.

Core claim

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, its behavioral predicates describe the effect.

What carries the argument

Behavioral predicates that summarize a function's possible aborts and state transitions, together with state labels that identify intermediate memory states for composing those predicates.

If this is right

Dynamic dispatch through stored or passed function values in Move contracts can now be verified directly.
SMT queries remain efficient because Move's static memory separation replaces the need for separation-logic encodings.
Annotation effort drops because weakest-precondition inference automatically produces behavioral-predicate specifications for higher-order code.
Verification pipelines for Aptos smart contracts can accept modules that use first-class functions without manual summaries.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same predicate-plus-label technique could be reused in other languages whose memory is partitioned into statically known regions.
Inference of behavioral predicates opens a route to verifying libraries that ship with higher-order entry points whose concrete callees are supplied later.
If the predicates are generated from source rather than supplied by the user, the approach would scale to whole-contract analysis without additional manual work.

Load-bearing premise

The behavioral predicates supplied for unknown function values correctly summarize every state change those functions can perform through references or globals.

What would settle it

A concrete Move program containing an unknown function value whose execution produces a state change outside the set described by its behavioral predicate, causing the SMT solver to accept an incorrect verification claim.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Move Prover extension for first-class imperative functions works via behavioral predicates but needs more evidence on soundness for unknown cases.

read the letter

This paper describes an extension to the Move Prover that lets it verify code using first-class functions which can be stored and called dynamically, including ones that change state. The new part is the behavioral predicates that characterize what a function does, covering aborts and pre/post conditions as single or two-state predicates. State labels help name intermediate memory states so predicates can be composed for sequences of transitions. On the SMT side, they discriminate: if the function value is known, use its direct effect; if unknown like a parameter or stored closure, fall back to the predicate. This supports imperative first-class functions that modify state through Rust-style references and global variables, which is more than Dafny handles. It also claims better efficiency than separation logic thanks to Move's static memory separation. They did well to extend the spec inference tool so it can generate these predicate-based specs from arbitrary higher-order code, which reduces manual work and gives a way to validate the new constructs. The soft spots are around the details of soundness. The abstract outlines the strategy but does not include concrete examples of the encoding or analysis of how complete the behavioral predicates are for all possible effects, such as reference aliasing to globals. The stress-test concern about unknown functions is reasonable; without seeing the full proofs or test cases, it's hard to be sure the predicates capture everything without gaps or over-approximations that could make verification unsound. That said, the approach builds on standard SMT techniques and Move's documented model, so no obvious circularity. This paper is for people building or using formal verifiers for smart contract languages, especially those dealing with dynamic features in Move on Aptos. A reader working on similar extensions for other languages would find the encoding strategy useful. It deserves a serious referee because it addresses a production language feature with a concrete implementation. I recommend sending it to peer review.

Referee Report

3 major / 2 minor

Summary. The paper extends the Move Prover (MVP) to support formal verification of imperative first-class functions in Move, which can be passed as values, stored, and enable dynamic dispatch. It introduces behavioral predicates (single-state or two-state) to characterize function aborts, pre/post-conditions, and effects, along with state labels to compose predicates over sequences of memory states. On the SMT level, the encoding discriminates known vs. unknown function values at call sites: concrete functions are inlined directly, while unknown ones (parameters or storage-loaded closures) are summarized via their behavioral predicates. The work also extends MVP's weakest-precondition inference to derive such specifications automatically. The central claim is that this handles state mutation via Rust-style references and globals (beyond Dafny) while yielding more efficient SMT encodings than separation logic due to Move's static memory separation.

Significance. If the behavioral-predicate encoding is shown sound and complete, the result would be a practical advance for verifying higher-order imperative smart contracts in Move. It directly addresses a new language feature (first-class functions with mutable state) and reduces annotation burden via inference, which is valuable for a production verifier. The efficiency argument tied to Move's memory model is a potential strength if demonstrated with concrete benchmarks.

major comments (3)

[§3] §3 (Behavioral Predicates): The definition of behavioral predicates for unknown function values relies on summarizing all possible aborts, pre/post conditions, and state modifications via references and globals, but no completeness argument or enumeration of possible aliasing behaviors is provided. If a reference aliasing a global or an abort condition is omitted, the SMT encoding becomes unsound for arbitrary closures loaded from storage.
[§4.1] §4.1 (SMT Encoding): The discrimination between known and unknown function values is described at a high level, but the paper provides no detailed translation rules or examples showing how state labels compose two-state predicates for sequences of reference mutations. This makes it impossible to verify that the encoding preserves the semantics of imperative effects.
[§5] §5 (Inference): The extension of weakest-precondition analysis to function values is claimed to reduce annotation burden, but no evaluation quantifies how often the inferred behavioral predicates are precise enough to discharge verification conditions without manual strengthening.

minor comments (2)

Notation for state labels (e.g., how they are attached to expressions) is introduced without a small grammar or example derivation in the main text.
The comparison to Dafny and separation logic in the abstract and introduction would benefit from a short table contrasting supported features (e.g., reference mutation, global variables, first-class functions).

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the detailed and constructive comments. We address each major point below and indicate the revisions we will make to strengthen the manuscript.

read point-by-point responses

Referee: [§3] §3 (Behavioral Predicates): The definition of behavioral predicates for unknown function values relies on summarizing all possible aborts, pre/post conditions, and state modifications via references and globals, but no completeness argument or enumeration of possible aliasing behaviors is provided. If a reference aliasing a global or an abort condition is omitted, the SMT encoding becomes unsound for arbitrary closures loaded from storage.

Authors: We agree that an explicit argument is needed. Move's type system and static memory separation ensure that references cannot alias globals or other unrelated storage locations; behavioral predicates are therefore defined only over the memory regions reachable from the function's declared parameters and captured state. We will add a dedicated paragraph in §3 that (1) recalls Move's aliasing restrictions, (2) shows that every possible abort, pre/post-condition, and effect is captured by the predicate signature, and (3) argues that no enumeration of impossible aliasing cases is required. This will be accompanied by a small illustrative example. revision: partial
Referee: [§4.1] §4.1 (SMT Encoding): The discrimination between known and unknown function values is described at a high level, but the paper provides no detailed translation rules or examples showing how state labels compose two-state predicates for sequences of reference mutations. This makes it impossible to verify that the encoding preserves the semantics of imperative effects.

Authors: We accept the criticism. We will insert a new subsection (or appendix) that presents the concrete SMT translation rules for function calls, including the handling of state labels (@pre, @post, etc.) when composing two-state predicates across reference mutations. Two worked examples—one with a known function and one with an unknown closure—will be added to demonstrate that the encoding preserves the intended semantics of imperative effects. revision: yes
Referee: [§5] §5 (Inference): The extension of weakest-precondition analysis to function values is claimed to reduce annotation burden, but no evaluation quantifies how often the inferred behavioral predicates are precise enough to discharge verification conditions without manual strengthening.

Authors: The manuscript presents the inference algorithm and illustrates its use on representative examples, but does not contain a quantitative benchmark suite measuring precision. Because the current work focuses on the design of the new specification constructs and the inference rules themselves, we do not believe a full empirical evaluation belongs in this paper. We will, however, add a short discussion in §5 that (a) explains why the rules are designed to be precise by construction for the supported Move constructs and (b) notes that a separate evaluation is planned for future work. revision: no

Circularity Check

0 steps flagged

No circularity in formal encoding of behavioral predicates

full rationale

The paper's derivation consists of an explicit SMT encoding that discriminates known function values (direct effect) from unknown ones (via behavioral predicates and state labels for composition). This construction is defined directly from Move's documented memory model and standard SMT techniques for higher-order functions, without any reduction of the central claim to fitted parameters, self-citations as load-bearing premises, or self-definitional loops. The approach is self-contained against external benchmarks such as Dafny and separation logic, with no equations or steps that equate the result to its inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The approach rests on standard assumptions about SMT solver capabilities and Move's static memory separation; new constructs are behavioral predicates and state labels.

axioms (2)

domain assumption SMT solvers can correctly handle discrimination over possible function values at call sites
Invoked for the encoding when the concrete function is unknown.
domain assumption Behavioral predicates faithfully capture all possible effects of a Move function including aborts and state changes
Central to both direct substitution and predicate-based reasoning.

invented entities (2)

behavioral predicates no independent evidence
purpose: Characterize Move functions by single-state or two-state predicates describing aborts and pre/post conditions
New specification construct introduced to handle first-class functions.
state labels no independent evidence
purpose: Name intermediate memory states to compose behavioral predicates for sequences of transitions
New mechanism for describing state evolution across function calls.

pith-pipeline@v0.9.0 · 5572 in / 1434 out tokens · 32622 ms · 2026-05-14T21:57:16.206777+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Combining Mechanical and Agentic Specification Inference for Move
cs.PL 2026-05 unverdicted novelty 6.0

Early prototype merges weakest-precondition analysis with an AI agent to infer Move specifications, using the prover as oracle to validate and refine them for code with loops, references, and higher-order functions.
Combining Mechanical and Agentic Specification Inference for Move
cs.PL 2026-05 unverdicted novelty 5.0

A hybrid tool pairs mechanical weakest-precondition analysis with an AI agent to infer verifiable specifications for Move programs, using the prover as an oracle to refine results until they pass.

Reference graph

Works this paper leans on

35 extracted references · 35 canonical work pages · cited by 1 Pith paper · 2 internal anchors

[1]

Fast and reliable formal verification of smart contracts with the move prover,

D. L. Dill, W. Grieskamp, J. Park, S. Qadeer, M. Xu, and J. E. Zhong, “Fast and reliable formal verification of smart contracts with the move prover,” inTools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), ser. Lecture Notes in Computer Science, vol. 13243. Springer, 2022, pp. 183–200

work page 2022
[2]

Resources: A safe language abstraction for money,

S. Blackshear, D. L. Dill, S. Qadeer, C. W. Barrett, J. C. Mitchell, O. Padon, and Y . Zohar, “Resources: A safe language abstraction for money,” 2020. [Online]. Available: https://arxiv.org/abs/2004.05106

work page arXiv 2020
[3]

The Move on Aptos Book,

Aptos Labs, “The Move on Aptos Book,” https://aptos-labs.github.io/ move-book/, 2023, accessed: 2026-05-09

work page 2023
[4]

Securing Aptos Framework with Formal Verifica- tion,

J. Park, T. Zhang, W. Grieskamp, M. Xu, G. D. Giacomo, K. Chen, Y . Lu, and R. Chen, “Securing Aptos Framework with Formal Verifica- tion,” in5th International Workshop on Formal Methods for Blockchains (FMBC 2024), ser. Open Access Series in Informatics (OASIcs), vol

work page 2024
[5]

9:1–9:16

Schloss Dagstuhl – Leibniz-Zentrum f ¨ur Informatik, 2024, pp. 9:1–9:16

work page 2024
[6]

The Aptos Framework Book,

Aptos Labs, “The Aptos Framework Book,” https://aptos-labs.github.i o/framework-book/, 2023, accessed: 2026-05-09

work page 2023
[7]

Move goes higher order,

W. Grieskamp, “Move goes higher order,” https://medium.com/aptosla bs/move-goes-higher-order-cdf9688a4919, Oct. 2025, aptos Labs blog

work page 2025
[8]

Trigger Selection Strategies to Stabilize Program Verifiers,

K. R. M. Leino and C. Pit-Claudel, “Trigger Selection Strategies to Stabilize Program Verifiers,” inProceedings of the 28th International Conference on Computer Aided Verification, Part I. Springer, 2016, pp. 361–381

work page 2016
[9]

The SMT-LIB Standard: Version 2.0,

C. Barrett, A. Stump, and C. Tinelli, “The SMT-LIB Standard: Version 2.0,” inProceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), A. Gupta and D. Kroening, Eds., 2010

work page 2010
[10]

Z3: an efficient SMT solver,

L. M. de Moura and N. Bjørner, “Z3: an efficient SMT solver,” in TACAS, ser. Lecture Notes in Computer Science, vol. 4963. Springer, 2008, pp. 337–340

work page 2008
[12]

Combining Mechanical and Agentic Specification Inference for Move

[Online]. Available: https://arxiv.org/abs/2605.10005

work page internal anchor Pith review Pith/arXiv arXiv
[13]

Higher-Order Paper Examples,

Aptos Labs, “Higher-Order Paper Examples,” https://github.com/aptos -labs/aptos-core/tree/d8be469f7f/third party/move/move-prover/doc/ higher-order-paper-26/examples, 2026, commitd8be469f7f, accessed 2026-05-11

work page 2026
[14]

The Move Prover,

J. E. Zhong, K. Cheang, S. Qadeer, W. Grieskamp, S. Blackshear, J. Park, Y . Zohar, C. Barrett, and D. L. Dill, “The Move Prover,” in Computer Aided Verification, S. K. Lahiri and C. Wang, Eds. Springer International Publishing, 2020, pp. 137–150

work page 2020
[15]

Boogie: A modular reusable verifier for object-oriented programs,

M. Barnett, B.-Y . E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino, “Boogie: A modular reusable verifier for object-oriented programs,” inInternational Symposium on Formal Methods for Components and Objects. Springer, 2005, pp. 364–387

work page 2005
[16]

This is boogie 2,

K. R. M. Leino, “This is boogie 2,” 2008, manuscript KRML 178. [Online]. Available: https://www.microsoft.com/en-us/research/publicati on/this-is-boogie-2-2/

work page 2008
[17]

Uniswap v2 core,

H. Adams, N. Zinsmeister, and D. Robinson, “Uniswap v2 core,” https: //uniswap.org/whitepaper.pdf, Mar. 2020, accessed: 2026-04-21

work page 2020
[18]

A polymorphic intermediate verifica- tion language: Design and logical encoding,

K. R. M. Leino and P. R ¨ummer, “A polymorphic intermediate verifica- tion language: Design and logical encoding,” inTACAS, J. Esparza and R. Majumdar, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010, pp. 312–327

work page 2010
[19]

Guarded commands, nondeterminacy and formal deriva- tion of programs,

E. W. Dijkstra, “Guarded commands, nondeterminacy and formal deriva- tion of programs,”Communications of the ACM, vol. 18, no. 8, pp. 453–457, 1975

work page 1975
[20]

Weakest-precondition of unstructured programs,

M. Barnett and K. R. M. Leino, “Weakest-precondition of unstructured programs,” inProceedings of the 6th ACM SIGPLAN-SIGSOFT Work- shop on Program Analysis for Software Tools and Engineering. New York, NY , USA: Association for Computing Machinery, 2005, pp. 82— 87

work page 2005
[21]

Move Prover Spec Inference Test Suite,

Aptos Labs, “Move Prover Spec Inference Test Suite,” https://github.c om/aptos-labs/aptos-core/tree/d8be469f7f/third party/move/move-prove r/tests/inference, 2026, commitd8be469f7f, accessed 2026-05-11

work page 2026
[22]

C. B. Jones,Systematic Software Development Using VDM, 2nd ed. Prentice-Hall, 1990

work page 1990
[23]

J. M. Spivey,The Z Notation: A Reference Manual, 2nd ed. Prentice- Hall, 1992

work page 1992
[24]

A computational model for Z based on concurrent con- straint resolution,

W. Grieskamp, “A computational model for Z based on concurrent con- straint resolution,” inZB 2000: Formal Specification and Development in Z and B, ser. Lecture Notes in Computer Science, J. P. Bowen, S. Dunne, A. Galloway, and S. King, Eds., vol. 1878. Springer, 2000, pp. 414–432

work page 2000
[25]

Abrial,The B-Book: Assigning Programs to Meanings

J.-R. Abrial,The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996

work page 1996
[26]

Verus: Verifying rust programs using linear ghost types,

A. Lattuada, T. Hance, C. Cho, M. Brun, I. Subasinghe, Y . Zhou, J. Howell, B. Parno, and C. Hawblitzel, “Verus: Verifying rust programs using linear ghost types,” inProc. ACM Program. Lang., vol. 7, no. OOPSLA1, 2023, pp. 286–315

work page 2023
[27]

Dependent types and multi-monadic effects in F*,

N. Swamy, C. Hrit ¸cu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. For- est, K. Bhargavan, C. Fournet, P.-Y . Strub, M. Kohlweiss, J.-K. Zinzin- doho´u´e, and S. Zanella-B ´eguelin, “Dependent types and multi-monadic effects in F*,” inProceedings of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 2016, p...

work page 2016
[28]

Dijkstra Monads for All

K. Maillard, D. Ahman, R. Atkey, G. Mart ´ınez, C. Hritcu, E. Rivas, and E. Tanter, “Dijkstra monads for all,” in24th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2019. [Online]. Available: https://arxiv.org/abs/1903.01237

work page internal anchor Pith review Pith/arXiv arXiv 2019
[29]

Accessible software verification with dafny,

K. M. Leino, “Accessible software verification with dafny,”IEEE Software, vol. 34, no. 06, pp. 94–97, nov 2017

work page 2017
[30]

The Lean 4 theorem prover and pro- gramming language,

L. de Moura and S. Ullrich, “The Lean 4 theorem prover and pro- gramming language,” inAutomated Deduction – CADE 28, ser. Lecture Notes in Computer Science, A. Platzer and G. Sutcliffe, Eds., vol. 12699. Springer, 2021, pp. 625–635

work page 2021
[31]

Nipkow, L

T. Nipkow, L. C. Paulson, and M. Wenzel,Isabelle/HOL: A Proof Assistant for Higher-Order Logic, ser. Lecture Notes in Computer Science. Springer, 2002, vol. 2283

work page 2002
[32]

Bertot and P

Y . Bertot and P. Cast ´eran,Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions, ser. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004

work page 2004
[33]

The Certora Prover,

Certora, “The Certora Prover,” https://www.certora.com/, 2024

work page 2024
[34]

SMT-Based Verification of Solidity Smart Contracts,

L. Alt and C. Reitwießner, “SMT-Based Verification of Solidity Smart Contracts,” inISoLA (4), ser. Lecture Notes in Computer Science, vol. 11247. Springer, 2018, pp. 376–388

work page 2018
[35]

solc-verify: A modular verifier for solidity smart contracts,

´A. Hajdu and D. Jovanovic, “solc-verify: A modular verifier for solidity smart contracts,”CoRR, vol. abs/1907.04262, 2019

work page arXiv 1907
[36]

SMT-Friendly Formalization of the Solidity Memory Model,

——, “SMT-Friendly Formalization of the Solidity Memory Model,” in ESOP, ser. Lecture Notes in Computer Science, vol. 12075. Springer, 2020, pp. 224–250

work page 2020