Formal Verification of Imperative First-Class Functions in Move

Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap +1

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: imperativ…