We present a toolchain for developing and verifying smart contracts that can be executed on Bitcoin. The toolchain is based on BitML, a recent domain-specific language for smart contracts with a computationally sound embedding into Bitcoin. Our toolchain automatically verifies relevant properties of contracts, among which liquidity, ensuring that funds do not remain frozen within a contract forever. A compiler is provided to translate BitML contracts into sets of standard Bitcoin transactions: executing a contract corresponds to appending these transactions to the blockchain. We assess our toolchain through a benchmark of representative contracts.
@article{arxiv.1905.07639,
title = {Developing secure Bitcoin contracts with BitML},
author = {Nicola Atzei and Massimo Bartoletti and Stefano Lande and Nobuko Yoshida and Roberto Zunino},
journal= {arXiv preprint arXiv:1905.07639},
year = {2019}
}