  The exploitation of smart-contract vulnerabilities can have catastrophic
consequences such as the loss of millions of pounds worth of crypto assets.
Formal verification can be a useful tool in identifying vulnerabilities and
proving that they have been fixed. In this paper, we present a formalisation of
Solidity and the Ethereum blockchain using the Solid language and its
blockchain; a Solid program is obtained by explicating/desugaring a Solidity
program. We make some abstractions that over-approximate the way in which
Solidity/Ethereum behave. Based on this formalisation, we create Solidifier: a
bounded model checker for Solidity. It translates Solid into Boogie, an
intermediate verification language, that is later verified using Corral, a
bounded model checker for Boogie. Unlike much of the work in this area, we do
not try to find specific behavioural/code patterns that might lead to
vulnerabilities. Instead, we provide a tool to find errors/bad states, i.e.
program states that do not conform with the intent of the developer. Such a bad
state, be it a vulnerability or not, might be reached through the execution of
specific known code patterns or through behaviours that have not been
anticipated.
