Formal Verification and the Holy Grail of Software Correctness

We present a formal model of Vyper that enables a fully formally verified compiler and proofs of important properties of smart contracts at the source level. This moves smart contract security beyond audits by making it possible to prove the correctness of the compiler and establish mathematical guarantees about contract behaviour.