@InProceedings{knispel_et_al:OASIcs.FMBC.2024.2, author = {Knispel, Andre and Melkonian, Orestis and Chapman, James and Hill, Alasdair and J\"{a}\"{a}ger, Joosep and DeMeo, William and Norell, Ulf}, title = {{Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda}}, booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)}, pages = {2:1--2:18}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-317-1}, ISSN = {2190-6807}, year = {2024}, volume = {118}, editor = {Bernardo, Bruno and Marmsoler, Diego}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.2}, URN = {urn:nbn:de:0030-drops-198673}, doi = {10.4230/OASIcs.FMBC.2024.2}, annote = {Keywords: blockchain, distributed ledgers, UTxO, Cardano, formal verification, Agda} }