Bitcoin smart contracts have historically been intentionally restricted to a small set of use cases, as its community prioritizes security and efficiency over expressiveness and feature completeness. BitML is a novel, domain-specific language for writing smart contracts which could bring greater flexibility to Bitcoin smart contracts. Its design is intended to enable the implementation of Turing-complete programs atop Bitcoin, with minimal changes to its core protocol.
A contract written in BitML is compiled to a set of standard Bitcoin transactions and executed on the blockchain. The power of BitML is that it guarantees a faithful execution of the high-level contract. Nothing is lost in translation. As a result, a developer using BitML can reason about the correctness of the BitML contract instead of having to analyze the resulting Bitcoin protocol. This means Bitcoin smart contracts can remain secure (and in alignment with the community’s security ethos) while having much broader applicability.
- Massimo Bartoletti is an Associate Professor at the Department of Mathematics and Computer Science of the University of Cagliari and has a Ph.D. in Computer Science at the University of Pisa.
- Roberto Zunino is an Adjunct Professor at the University of Trento where he focuses on formal techniques for cryptographic protocol analysis and with an emphasis on blockchain systems.
- The following authors have also contributed to the body of research that supports BitML: Stefano Lande, Nicola Atzei, Nobuko Yoshida, and Maurizio Murgia.
Q1: Are you aware of groups/companies using BitML to design real-world Bitcoin smart contracts nowadays? If not, what are the main obstacles that you currently see hindering deployment?
A: Although we are not aware of any attempt to use BitML in the wild, we are in touch with blockchain companies which are developing new UTXO-based smart contract languages inspired by the BitML design. In our view, the main obstacle that hinders the adoption of BitML is its limited expressiveness, which is a direct consequence of using Bitcoin as a compilation target. Indeed, our primary goal when designing BitML was executing BitML contracts in Bitcoin as-is, without using non-standard transactions or relying on sidechains, like RSK or Elements. The good news is that the expressiveness of BitML can be significantly increased with minimal extensions of the compilation target: for instance, adding covenants to Bitcoin would make it possible to have a (nearly) Turing-complete language. We discuss this point more in detail below.
Q2: In a follow-up work, you created a toolchain; what is the amount of knowledge/expertise expected from protocol designers to use this toolchain?
A: BitML is easy to learn: it only has a handful of constructs, each one having an intuitive semantics. Even if it is different from everyday programming languages, developers should be able to understand how to use it in a few hours.
On the other hand, designing a smart contract for a complex task can be challenging, whether one is using BitML or not. This is because one needs to ensure that the contract behaves correctly not only when run by honest participants, but also in the presence of adversaries. Fair gambling games, for instance, are notoriously hard to design. The verifier included in the tool chain helps designers verify complex contracts. For instance, it is possible to ensure that in no case the currency can get “frozen” inside the contract, or that honest players eventually get their collateral back.
Q3: How easy is it to specify meaningful correctness and security properties for Bitcoin smart contracts?
A: Currently, BitML supports the verification of two kinds of properties: liquidity, and linear temporal logic (LTL) properties. Specifying liquidity is straightforward, since the query language features a dedicated construct for this property. Specifying LTL properties instead requires a basic understanding of LTL, which perhaps is not among the skills of average developers.
Q4: The current soundness result for BitML covers trace properties. Do you think that there is the possibility to extend this result to broader property classes (like hyperproperties)?
A: We believe that it is possible to extend our results to cover branching-time properties, such as those expressible in CTL, or even in the probabilistic logic PCTL. We are working in this direction right now.
Extending our results to hyperproperties could be possible, but at this moment it seems difficult to do without neglecting the probabilistic aspects of the BitML transition system.
Q5: Do you consider it a possibility to add support for quantitative or probabilistic reasoning to BitML (e.g., to reason about the winning chances/expected outcomes of parties in a contract)?
A: Some forms of quantitative reasoning are already available. For instance, in BitML we can verify that a participant can eventually redeem at least a certain amount of currency from the contract. Further, in some cases it is possible to automate the verification of fairness: we did this, for instance, for a lottery contract. In the general case, though, it seems hard to verify that a game contract is fair, or that the expected payoffs of the participants are the intended ones.
We are currently working on supporting more probabilistic reasoning in BitML, using the PCTL logic to express some probabilistic properties of interest.
Q6: BitML currently is, as you describe, not “Bitcoin-complete”. Are there concrete plans to extend BitML to a “Bitcoin-complete” language?
A: BitML is not Bitcoin-complete, in the sense that there exist contracts which are executable in Bitcoin but are not expressible in BitML. The main sources of incompleteness are two:
- off-chain interactions are limited to stipulation, revealing secrets and providing authorizations. In particular, stipulation requires that all the transactions obtained by the BitML compiler must be signed by all the participants before the contract starts.
- partial signatures (like those obtained through SIGHASH_ANYONECANPAY and SIGHASH_SINGLE) are not used.
As a consequence of the design choices above, contracts with a dynamically-defined set of players, or an unbounded number of iterations, are not expressible in BitML.
Recently, we have proposed an extension of BitML ([2011.14165] Verification of recursive Bitcoin contracts) which partially overcomes the first limitation. More precisely, the extended BitML allows participants to “renegotiate” a contract at run-time. Besides allowing participants to provide new deposits and to commit to new secrets at run-time, renegotiation also allows for “consensual” recursion, still admitting compilation to standard Bitcoin transactions, and a sound analysis for contract liquidity.
Relaxing also the other constraint would allow to further extend the expressiveness of BitML. For instance, recursion and partial signatures enable crowdfunding contracts, and more complex off-chain protocols enable micro-payment channels. Notably, these extensions could be implemented without modifying Bitcoin.
Q7: Do you see applications for Bitcoin competing with Ethereum as a smart contract platform (with the introduction of covenants)?
A: It is difficult to predict which platform will win this competition, since this depends on many factors besides the effectiveness of the smart contracts machinery (not mentioning the impact on the competition of emerging blockchain platforms like Cardano and Algorand, to cite a few).
However, abstracting from the actual blockchain platform, we envision a competition between stateless and stateful smart contracts. Both types of design have pros and cons. On the one hand, programming contracts in a stateful model (like in Ethereum) is perhaps more natural for most developers, whereas encoding state in a stateless model (like we do in BitML) requires a different way of thinking. On the other hand, the stateless UTXO model (like Bitcoin’s) simplifies the blockchain design, as the global state of the blockchain is just the set of unspent transaction outputs. This has a direct consequence on scalability and throughput, since more transactions can be executed concurrently. Another advantage of the stateless approach is that it seems more amenable to verification. For instance, BitML features a sound and complete verification technique for contract liquidity.
Q8: How do you see the future of extensions of the Bitcoin scripting language for more efficient Bitcoin smart contracts? Which would be the specific additions to the language that you would promote?
A: In general, we believe that adding covenants would be crucial to enable a large class of Bitcoin smart contracts. Covenants may come in many flavors, and the recent BIP119 proposes one of them. We also proposed our own flavor of covenants in https://arxiv.org/abs/2006.03918. Our covenants allow Bitcoin scripts to inspect the transactions in their neighborhood, i.e. those which are close in the transaction graph. For instance, we have shown that our covenants would allow Bitcoin to support fungible tokens efficiently.
Further, it would be nice to have “user data” fields in transactions, where one can store the current state of the contract, and ensure state invariants using covenants. These stateful contracts could require large scripts, exceeding the current 520 bytes limit. The adoption of Taproot would mitigate this issue, by allowing transactions to witness only the part of the contract to be executed.
Crucially, these extensions would keep the feature that scripts are run in constant time, so avoiding to resort to a “gas” mechanism as in Ethereum.
- We’d like to thank the authors of BitML for their work on this topic over the years and for taking the time to write such thoughtful answers.
- SCRF is also thankful to @clara.schneidewind for contributing to the questions posed to the authors and for writing an excellent summary on BitML.
- As covered in the interview, BitML can be instrumental in increasing the usage of smart contracts on Bitcoin through a set of trade-offs that are compatible with the ethos of its community.
- Taproot has been mostly overlooked because, as a foundational technology, it is difficult for the average user to envision some of the use-cases it enables.
- However, as discussed here and in our previous summaries, Taproot may serve as a building block for the adoption of languages such as BitML, which can push Bitcoin’s functionality closer to Turing-completeness.