In this post, we demonstrate how Internet Computer developers can leverage automatic verification to build bug-free, Web3 applications in Motoko. We start by explaining why this is tricky. We then demonstrate an example smart contract (a.k.a. canister in Motoko), showing how to formally specify and (automatically) verify it. We conclude with a discussion of our experience and observations gathered while working on this (very experimental) verification technique.
We wrote this post because we wanted to make more of DFINITY's formal verification know-how available to developers outside the Foundation. While DFINITY employs verification experts to formally specify and verify some of our smart contracts, we believe that formal verification is beneficial to all Web3 projects, especially in high-stake applicatio