Is Formal Verification Practical?

Abstract

There is arguably no other domain in which the prospect of formal verification is as promising as in the area of smart contracts. Smart contracts are small- to medium-sized programs which are strongly isolated from external components. They handle high-value digital assets, and correctness is of utmost importance. Many large-impact bugs and exploits have been documented over the years. Bug bounty programs for contracts are common in the industry, offering awards in the millions of dollars, making the cost of bugs exorbitant, and the motivation for better solutions high. Move is a newer smart contract language used by multiple blockchains and has been designed at Meta from the ground up with formal verification in mind, featuring an integrated specification language and semantics well suited for formal reasoning. This opportunity resulted in the Move Prover [1], a tool that has been successfully used in the exhaustive formal verification of Diem at Meta, as well as for the frameworks of the Aptos protocol [2]. However, even though extensive work has been invested in the Move Prover to make it feasible for regular developers, most applications of the prover required specifically skilled engineers and tedious detail work to succeed, preventing it from going mainstream. In this talk, we explore the state-of-the-art of formal verification for Move. We identify the challenges that users face when trying to apply formal verification and point out future research directions to improve the expressiveness and usability of the Move Prover.