The adoption of blockchain based distributed ledgers is growing
fast due to their ability to provide reliability, integrity, and auditability
without trusted entities. One of the key capabilities of these emerging
platforms is the ability to create self-enforcing smart contracts. However,
the development of smart contracts has proven to be error-prone in practice,
and as a result, contracts deployed on public platforms are often
riddled with security vulnerabilities. This issue is exacerbated by the design
of these platforms, which forbids updating contract code and rolling
back malicious transactions. In light of this, it is crucial to ensure that a
smart contract is secure before deploying it and trusting it with significant
amounts of cryptocurrency. To this end, we introduce the VeriSolid
framework for the formal verification of contracts that are specified using
a transition-system based model with rigorous operational semantics.
Our model-based approach allows developers to reason about and verify
contract behavior at a high level of abstraction. VeriSolid allows the
generation of Solidity code from the verified models, which enables the
correct-by-design development of smart contracts