Formal Verification of Smart Contracts

The paper outline a framework to analyze and verify both the runtime safety and the functional correctness of Solidity contracts in F*, a functional programming language aimed at program verification.