CERIAS Security Seminar: Fast and Reliable Formal Verification of Smart Contracts with the Move Prover

The Center for Education and Research in Information Assurance and Security
November 30, 2022
4:30 PM - 5:30 PM
STEW G52 (Suite 050B), West Lafayette Campus


Meng Xu
University of Waterloo


The Move Prover (MVP) is a formal verifier forsmart contracts written In the Move programming language. MVP has an expressivespecification language, and is fast and reliable enough that it can be runroutinely by developers and in integration testing. Besides the simplicity ofsmart contracts and the Move language, three implementation approaches areresponsible for the practicality of MVP: (1) an alias-free memory model, (2)fine-grained invariant checking, and (3) monomorphization. The entirety of theMove code for the Diem blockchain has been extensively specified and can becompletely verified by MVP in a few minutes. Changes in the Diem framework mustbe successfully verified before being integrated into the open sourcerepository on GitHub.


Dr.Meng Xu is an Assistant Professor in the Cheriton School of Computer Science atthe University of Waterloo, Canada. His research is in the area of system andsoftware security, with a focus on delivering high-quality solutions topractical security programs, especially in finding and patching vulnerabilitiesin critical computer systems. This usually includes research and development ofautomated program analysis/ testing / verification tools that facilitate thesecurity reasoning of critical programs.

The weekly security seminar has been held every semester since spring of 1992. We invite personnel at Purdue and visitors from outside to present on topics of particular interest to them in the areas of computer and network security, computer crime investigation, information warfare, information ethics, public policy for computing and security, the computing "underground," and other related topics. More info

Contact Details

Event Website


Add to calendar