  Derivatives are a special type of financial contracts used to hedge risks or
to speculate on the market fluctuations. In order to avoid ambiguities and
misinterpretations, several domain specific languages (DSLs) for specifying
such derivatives have been proposed. The recent development of the blockchain
technologies enables the automatic execution of financial derivatives. Once
deployed on the blockchain, a derivative cannot be modified. Therefore, more
caution should be taken in order to avoid undesired situations.
  In this paper, we address the formal verification of financial derivatives
written in a DSL for blockchain, called Findel. We identify a list of
properties that, once proved, they exclude several security vulnerabilities
(e.g., immutable bugs, money losses). We develop an infrastructure that
provides means to interactively formalize and prove such properties. To provide
a higher confidence, we also generate proof certificates. We use our
infrastructure to certify non-trivial examples that cover the most common types
of derivatives (forwards/futures, swaps, options).
