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 made available a preprint describing out toolchain, and a short video demonstration.

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

Warning

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

References

[CCS18]
  1. Bartoletti, R. Zunino. BitML: A Calculus for Bitcoin Smart Contracts. In ACM SIGSAC CCS, 2018. Preprint: https://eprint.iacr.org/2018/122.pdf
[POST19]
  1. Bartoletti, R. Zunino. Verifying liquidity of Bitcoin contracts. In Principles of Security and Trust (POST), 2019. Preprint: https://eprint.iacr.org/2018/1125.pdf
[RACKET]https://racket-lang.org/
[MAUDE]http://maude.cs.illinois.edu/w/index.php/The_Maude_System http://maude.sip.ucm.es/strategies/