BitML Toolchain¶

BitML is a domain-specific language for Bitcoin smart contracts, introduced in [CCS18]. The BitML toolchain implements:

an IDE for developing BitML contracts, integrated in the DrRacket IDE [RACKET];
a compiler which translates BitML contracts into standard Bitcoin transaction. The compiler is computationally sound, meaning that computational attacks (i.e., at the level of Bitcoin transactions) can be detected at the symbolic level of the BitML semantics;
a model checker which verifies security properties of BitML contracts, like their liquidity (i.e., funds never remain frozen in a contract [POST19]), and custom LTL properties. The model checker is based on Maude [MAUDE].

We published a paper [ESEC] describing out toolchain, accompanied by a short video demonstration. We also presented the BitML toolchain at Scaling Bitcoin 2019 (video).

The BitML toolchain is developed by the Blockchain@Unica group of the University of Cagliari. The project is open source, and you are welcome to contribute to its repositories.

Contents¶

BitML Tutorial

Smart contracts

Warning

BitML is intended for research purposes only. Do not use it to create mainnet transactions, or do it at your own risk.

Bartoletti, R. Zunino. BitML: A Calculus for Bitcoin Smart Contracts. In ACM SIGSAC CCS, 2018. Preprint: https://eprint.iacr.org/2018/122.pdf

Bartoletti, R. Zunino. Verifying liquidity of Bitcoin contracts. In Principles of Security and Trust (POST), 2019. Preprint: https://eprint.iacr.org/2018/1125.pdf

Atzei, M. Bartoletti, S. Lande, N. Yoshida, R. Zunino. Developing secure Bitcoin contracts with BitML. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). https://dl.acm.org/doi/pdf/10.1145/3338906.3341173