Formalizing IOTA Extended UTXO in Isabelle

Abstract

The IOTA Extended UTXO (IOTA EUTXO) model extends the UTXO blockchain to include features like smart contracts and non-fungible tokens. In this work, we show that the IOTA EUTXO model maintains the base correctness properties of the UTXO model while extending it with extra functionality. We achieve this by specifying and verifying the essential concepts of the base UTXO model and the extensions proposed by IOTA using the Isabelle proof assistant. The specification is designed to be modular and extensible, meaning it can be used as a foundation for further research of the UTXO and IOTA EUTXO models.