3 papers
cs.PL2026
Defense-in-Depth Runtime Safety in Move
Victor Gao, Wolfgang Grieskamp, Vineeth Kashyap +5
Move is a smart-contract language used to execute transactions on the Aptos blockchain. Move programs execute in a sandboxed VM as typed bytecode. The VM statically verifies founda…
cs.PL2026
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…
cs.PL2026
Combining Mechanical and Agentic Specification Inference for Move
Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap
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 co…