  Smart contracts are the artifact of the blockchain that provide immutable and
verifiable specifications of physical transactions. Solidity is a
domain-specific programming language with the purpose of defining smart
contracts. It aims at reducing the transaction costs occasioned by the
execution of contracts on the distributed ledgers such as the Ethereum.
However, Solidity contracts need to adhere safety and security requirements
that require formal verification and certification. This paper proposes a
method to meet such requirements by translating Solidity contracts to Event-B
models, supporting certification. To that purpose, we define a restrained
Solidity subset and a transfer function which translates Solidity contracts to
Event-B models. Then we take advantage of Event-B method capabilities to refine
models at different levels of abstraction to verify Solidity contracts'
properties. And we can verify the generated proof obligations of the Event-B
model with the help of the Rodin platform.
