1. Introduction
Bitcoin's Unspent Transaction Output (UTXO) model, while elegant for concurrent currency transfer, presents significant limitations for implementing complex, stateful smart contracts due to its lack of shared mutable state. Covenants emerge as a critical linguistic primitive proposed to extend Bitcoin Script, allowing a transaction to impose constraints on the scripts of future redeeming transactions. This paper addresses the gap in formal, abstract models for covenants, which have been described primarily from a low-level, implementation-focused perspective since their inception around 2013. By providing a formal foundation, the work aims to simplify reasoning about contract properties, enable the specification of advanced use cases beyond Bitcoin's current capabilities, and facilitate the design of higher-level programming abstractions.
2. The Pure Bitcoin Model
The paper adapts a formalization of the core Bitcoin transaction model. In the UTXO model, the blockchain state is defined by a set of unspent transaction outputs. Each output contains a value (amount of bitcoin) and a scriptPubKey (locking script) that specifies the conditions required to spend it. A spending transaction provides a scriptSig (unlocking script) and references the UTXO it wishes to consume. Validation involves executing the concatenated scripts. Crucially, standard Bitcoin Script is limited: it cannot introspect or constrain the structure of the spending transaction beyond signature verification and basic arithmetic/logic, preventing the creation of contracts that enforce multi-step protocols.
3. Formal Model of Covenants
The core contribution is a formal model that abstracts proposed covenant opcodes (like OP_CHECKTEMPLATEVERIFY).
3.1. Covenant Primitives & Syntax
The model introduces covenant predicates as extensions to Bitcoin Script. A covenant is essentially a constraint $C(T_x, T_{next})$ that evaluates to true or false, where $T_x$ is the current transaction being spent and $T_{next}$ is the proposed spending transaction. The predicate can inspect fields of $T_{next}$, such as its output scripts, amounts, or locktimes.
3.2. Operational Semantics
The validation rule is extended: For a UTXO with a covenant, the validation of a spending transaction $T_{next}$ requires not only that its scriptSig satisfies the original scriptPubKey but also that the covenant predicate $C$ holds for the pair $(T_x, T_{next})$. This is formally defined using operational semantics rules that integrate covenant checking into the existing Bitcoin validation logic.
3.3. Recursive Covenants & State Machines
A powerful variant is the recursive covenant, where $C$ can enforce that $T_{next}$'s output itself contains the same (or a related) covenant $C'$. This enables the implementation of state machines on Bitcoin: each transaction represents a state transition, with the covenant ensuring the state machine rules are followed across a chain of transactions. The paper formalizes this as a sequence of transactions $T_1, T_2, ..., T_n$ where for each $i$, $C(T_i, T_{i+1})$ holds.
4. Specifying Complex Bitcoin Contracts
The formal model is applied to specify contracts currently inexpressible or cumbersome in pure Bitcoin.
4.1. Vaults & Time-Locked Withdrawals
Covenants can create "vaults" where stolen funds can be recovered. A transaction can require that any large withdrawal must first go to a time-locked output, allowing the owner to cancel it if it was unauthorized. This is specified by a covenant that checks the nLockTime field and output structure of $T_{next}$.
4.2. Payment Channels & Lightning Network
While Lightning Network exists, covenants can simplify and secure its underlying construction. They can enforce that a channel's closing transaction must be the most recent state, preventing old state broadcasts, by constraining the spending transaction to match a pre-signed update.
4.3. Decentralized Finance (DeFi) Primitives
Simple DeFi constructs like collateralized debt or non-custodial swaps become possible. A covenant can lock funds in a transaction that can only be spent by a transaction presenting a valid cryptographic proof of payment from a counterparty or of liquidation.
5. High-Level Language Primitives
The paper discusses how covenants can serve as a compilation target for high-level contract languages. Primitives like "withdraw after time T", "spend only if counterparty signs", or "transition state from A to B" can be directly mapped to specific covenant constraints, raising the abstraction level for Bitcoin contract developers.
6. Core Insight & Analyst's Perspective
Core Insight: Bartoletti et al. aren't just proposing another covenant opcode; they're delivering the missing formal theory that turns a clever hack into a legitimate, analyzable programming paradigm for Bitcoin. This is the key that unlocks systematic engineering of complex, secure contracts on UTXO blockchains, moving beyond ad-hoc scripting.
Logical Flow: The argument is compellingly simple: 1) Bitcoin's UTXO model lacks state, limiting contracts. 2) Covenants proposed as a fix are poorly understood formaly. 3) Therefore, we build a formal model. 4) Using this model, we demonstrate it can express valuable, complex use cases (vaults, channels, DeFi). 5) This formalism then naturally enables higher-level language design. It's a classic "theory enables practice" pipeline executed with precision.
Strengths & Flaws: The major strength is bridging the gap between cryptography/PL theory and Bitcoin engineering—a gap that has led to costly bugs in Ethereum's account-based model. The formal semantics allow for property verification, a huge win. The flaw, acknowledged implicitly, is the political economy of Bitcoin. As the paper notes, Bitcoin's "extremely cautious approach" makes deploying new opcodes like covenants a herculean task, regardless of their formal elegance. The success of Layer-2s like Lightning without native covenants also raises questions about necessity versus nicety. Furthermore, the model's security rests on the assumption that the constrained fields (like script hashes) are sufficient; unforeseen interaction effects with other opcodes could remain.
Actionable Insights: For researchers, this paper is a blueprint: use formal methods to de-risk and clarify blockchain upgrades. For developers, start designing contract frameworks now assuming covenants will exist (as seen on Liquid or Stacks). For Bitcoin protocol developers, the paper provides the rigorous foundation needed to argue for BIP 119 (OP_CTV) or similar proposals—it transforms a feature request into an engineering specification. The biggest takeaway: the future of Bitcoin smart contracts isn't about mimicking Ethereum, but about leveraging the unique UTXO+covenants paradigm to create a new, potentially more secure and scalable, class of decentralized applications.
7. Technical Details & Formalization
The formal model defines transactions, scripts, and validation contextually. A key technical detail is the representation of the covenant constraint. Let $\texttt{tx}$ represent a transaction. A covenant can be seen as a function:
$\text{Covenant}_{\text{cond}} : \texttt{tx}_{\text{current}} \times \texttt{tx}_{\text{next}} \times \sigma \rightarrow \{\text{True}, \text{False}\}$
where $\sigma$ represents the validation context (block height, etc.). The predicate $\text{cond}$ can be a conjunction of checks on $\texttt{tx}_{\text{next}}$ fields:
$\text{cond} \equiv (\texttt{hashOutputs}(\texttt{tx}_{\text{next}}) = H) \land (\texttt{nLockTime}(\texttt{tx}_{\text{next}}) > T) \land ...$
This aligns with proposals like OP_CHECKTEMPLATEVERIFY, which pushes a hash of specified parts of the spending transaction onto the stack for comparison. The recursive property is formalized by ensuring an output of $\texttt{tx}_{\text{next}}$ contains a script $S'$ that itself enforces a covenant $\text{Covenant}_{\text{cond}'}$.
8. Analysis Framework & Example Case
Example: A Simple Vault Contract
Goal: Create a UTXO that can be spent in two ways: 1) Instantly, but only to a specific "cold storage" address. 2) To any address, but only after a 30-day delay (allowing cancellation of theft).
Framework Application using the Formal Model:
1. Initial Locking Script (scriptPubKey): Contains a covenant condition $C_1$.
2. Covenant $C_1(T_{vault}, T_{spend})$: Must evaluate to True. It checks:
a) Path A (Instant): $\texttt{hashOutputs}(T_{spend}) = H_{cold}$ // Output must hash to pre-committed cold storage address.
b) Path B (Delayed): $\texttt{nLockTime}(T_{spend}) \geq \text{currentBlock} + 4320$ (30 days in blocks) AND $\texttt{hashOutputs}(T_{spend})$ can be anything.
3. Validation: When spending the vault UTXO with $T_{spend}$, the Bitcoin node executes the script. It requires a signature from the vault owner and verifies that $C_1$ holds for the transaction pair.
This example demonstrates how the formal model's predicate $C(T_x, T_{next})$ is instantiated with concrete checks on the next transaction's fields, enabling a security property (theft recovery) impossible in base Bitcoin.
9. Future Applications & Directions
The formalization opens several future avenues:
- Verified Compilers: Building compilers from high-level languages (like Simplicity or Miniscript extensions) to covenant-embedded Bitcoin Script, with formal proofs of correctness.
- Cross-Chain Covenants: Exploring covenants that condition spends on events from other blockchains or oracles, using cryptographic proofs like SPVs, as hinted by earlier work on "bridges" and recent research on rollups.
- Privacy-Preserving Covenants: Integrating covenant checks with zero-knowledge proofs (e.g., using Taproot/Schnorr signatures) to hide the contract logic while still enforcing it, a direction being explored in projects like Ark.
- Formal Security Analysis: Using the model to systematically analyze the security of proposed covenant constructions against economic and cryptographic attacks, similar to the work done on Ethereum's smart contracts by the IEEE Symposium on Security and Privacy community.
- Layer-2 Protocol Simplification: Redesigning protocols like the Lightning Network or sidechains (Liquid) to be more efficient and trust-minimized by leveraging native covenants, reducing the need for complex watchtowers or federations.
10. References
- M. Bartoletti, S. Lande, R. Zunino. Bitcoin covenants unchained. arXiv:2006.03918v2 [cs.PL]. 2020.
- S. Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System. 2008.
- J. Poon, T. Dryja. The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments. 2016.
- M. Moser, I. Eyal, E. G. Sirer. Bitcoin Covenants. Financial Cryptography 2016 Workshops.
- Bitcoin Improvement Proposal 119 (BIP 119). OP_CHECKTEMPLATEVERIFY.
- G. Wood. Ethereum: A Secure Decentralised Generalised Transaction Ledger. Ethereum Yellow Paper. 2014.
- A. Miller, et al. Hashed Timelock Contracts (HTLCs). 2017.
- R. O'Connor. Simplicity: A New Language for Blockchains. Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security.
- Blockstream. Liquid Network. https://blockstream.com/liquid/
- IEEE Symposium on Security and Privacy. Multiple papers on smart contract security analysis. Various years.