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].
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