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