  Smart contracts are a special type of programs running inside a blockchain.
Immutable and transparent, they provide means to implement fault-tolerant and
censorship-resistant services. Unfortunately, its immutability causes a serious
challenge of ensuring that a business logic and implementation is correct
upfront, before publishing in a blockchain. Several big accidents have indeed
shown that users of this technology need special tools to verify smart contract
correctness. Existing automated checkers are able to detect only well known
implementation bugs, leaving the question of business logic correctness far
aside. In this work, we present a symbolic model-checking technique along with
a formal specification method for a subset of Solidity programming language
that is able to express both state properties and trace properties; the latter
constitutes a weak analogy of temporal properties. We evaluate the proposed
technique on the MiniDAO smart contract, a young brother of notorious TheDAO.
Our Proof-of-Concept was able to detect a non-trivial error in the business
logic of this smart contract in a few seconds.
