David L. Dill
David L. Dill is a Lead Researcher at Facebook, working on the Diem blockchain project. He is also Donald E. Knuth Professor, Emeritus, in the School of Engineering at Stanford University. He was on the faculty in the Department of Computer Science at Stanford from 1987 until becoming emeritus in 2017. Prof. Dill’s research interests include formal verification of software, hardware, and protocols, with a focus on automated techniques, as well as voting technology and computational biology. For his research contributions, he has received a CAV award and Alonzo Church award. He is an IEEE Fellow, an ACM Fellow and a member of the National Academy of Engineering and the American Academy of Arts and Sciences. He also received an EFF Pioneer Award for his work in voting technology and is the founder of VerifiedVoting.org, an organization that champions trustworthy elections.
Formal verification of Move programs for the Diem blockchain
The Diem blockchain, which was initiated in 2018 by Facebook, includes a novel programming language called Move for implementing smart contracts. The correctness of Move programs is especially important because the blockchain will host large amounts of assets, those assets are managed by smart contracts, and because there is a history of large losses on other blockchains because of bugs in smart contracts. The Move language is designed to be as safe as we can make it, and it is accompanied by a formal specification and automatic verification tool, called the Move Prover. The Diem Framework is the Move code that makes up the core logic of the Diem blockchain, managing accounts, payments, etc. Extensive formal specifications have been written for the most important properties of the Framework, all of which can be formally verified by the Move Prover in less than 40 seconds per file. Indeed, the framework is re-verified automatically in continuous integration whenever new code is submitted to Github. The entire blockchain implementation, including the Move language, virtual machine, the Move Prover, and near-final various Move modules are available on https://github.com/diem/diem.
This talk will be about the goals of the project and the most interesting insights we’ve had as of the time of the presentation.