On the Formal Verification of Smart Contracts and Blockchain: Challenges and Future Directions

The introduction of blockchain technology and smart contracts has fundamentally transformed multiple industries, offering improved security, transparency, and automation. Nevertheless, guaranteeing the security and correctness of these systems continues to be a crucial challenge. Existing formal methods enable the blockchain and smart contract developers to i) provide an abstract model of the systems; ii) specify the important properties that must be maintained in the systems, e.g., safety, correctness, and security; and iii) verify that the proposed abstract model fulfills the property specification. Thus, avoid costly errors that can occur in the future and take anticipation measures. This work explores the utilization of three basic formal methods, namely model checking, theorem proving, and formal verification through translation to <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\boldsymbol{F^{*}}$</tex> programming language, to verify and confirm the correctness and security of blockchain systems and smart contracts functionality.