ASC2021 - Formal Verification of Smart Contracts - MSSASSI Souhail

A smart contract is written in a programming language (commonly Solidity) and then translated into bytecodes. Once a smart contract is reduced to bytecodes, it can be deployed on the blockchain as a contract account at some address. Once deployed no one can change it or apply a patch to it.We should have great confidence that the contract will behave correctly no matter what.
Formal verification is essentially concerned with identifying the correctness of hardware and software design operation. Because verification uses formal mathematical proofs, a suitable mathematical model of the design must be created.