# Modelling Bitcoin in Agda

arXiv: https://arxiv.org/abs/1804.06398 · HTML: https://mlsanity.com/paper/1804.06398/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Apr 2018.

## Built on by (most cited first, 2 of 2)

- [Towards Automating Blockchain Consensus Verification with IsabeLLM](https://mlsanity.com/paper/2601.07654/) (2026)
- [IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus](https://mlsanity.com/paper/2606.18098/) (2026)

## Abstract (arXiv)

We present two models of the block chain of Bitcoin in the interactive theorem prover Agda. The first one is based on a simple model of bank accounts, while having transactions with multiple inputs and outputs. The second model models transactions, which refer directly to unspent transaction outputs, rather than user accounts. The resulting blockchain gives rise to a transaction tree. That model is formalised using an extended form of induction-recursion, one of the unique features of Agda. The set of transaction trees and transactions is defined inductively, while simultaneously recursively defining the list of unspent transaction outputs. Both structures model standard transactions, coinbase transactions, transaction fees, the exact message to be signed by those spending money in a transaction, block rewards, blocks, and the blockchain, and the second structure models as well maturation time for coinbase transactions and Merkle trees. Hashing and cryptographic operations and their correctness are dealt with abstractly by postulating corresponding operations. An indication is given how the correctness of this model could be specified and proven in Agda.