# Developing secure Bitcoin contracts with BitML

## TL;DR

This paper introduces a toolchain for creating and verifying secure Bitcoin smart contracts using BitML, enabling automatic property verification and translation into Bitcoin transactions for practical deployment.

## Contribution

It presents a novel toolchain that integrates a domain-specific language, property verification, and compilation into Bitcoin transactions, enhancing security and reliability of Bitcoin smart contracts.

## Key findings

- Automated verification of contract properties like liquidity.
- Successful translation of BitML contracts into executable Bitcoin transactions.
- Benchmark results demonstrating effectiveness on representative contracts.

## Abstract

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.