  This paper introduces WhylSon, a deductive verification tool for smart
contracts written in Michelson, which is the low-level language of the Tezos
blockchain. WhylSon accepts a formally specified Michelson contract and
automatically translates it to an equivalent program written in WhyML, the
programming and specification language of the Why3 framework. Smart contract
instructions are mapped into a corresponding WhyML shallow-embedding of the
their axiomatic semantics, which we also developed in the context of this work.
One major advantage of this approach is that it allows an out-of-the-box
integration with the Why3 framework, namely its VCGen and the backend support
for several automated theorem provers. We also discuss the use of WhylSon to
automatically prove the correctness of diverse annotated smart contracts.
