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.