Search Results

Documents authored by Ferariu, Tudor

Artifact
Software
DOI: 10.4230/artifacts.23006
tferariu/agda2plinth

Authors: Tudor Ferariu, Philip Wadler, and Orestis Melkonian

Abstract
Cite as

Tudor Ferariu, Philip Wadler, Orestis Melkonian. tferariu/agda2plinth (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23006,
   title = {{tferariu/agda2plinth}}, 
   author = {Ferariu, Tudor and Wadler, Philip and Melkonian, Orestis},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:03dd5b9f802117f3b5ccef0ed56d4214fee41238}{\texttt{swh:1:dir:03dd5b9f802117f3b5ccef0ed56d4214fee41238}} (visited on 2025-05-16)},
   url = {https://github.com/tferariu/agda2plinth},
   doi = {10.4230/artifacts.23006},
}
Document
DOI: 10.4230/OASIcs.FMBC.2025.6
Validity, Liquidity, and Fidelity: Formal Verification for Smart Contracts in Cardano

Authors: Tudor Ferariu, Philip Wadler, and Orestis Melkonian

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract
Good news for researchers in formal verification: smart contracts regularly suffer exploits such as the DAO bug, which lost the equivalent of 60 million USD on Ethereum. This makes a strong case for applying formal methods to guarantee essential properties. Which properties would we like to prove? Most previous studies focus on contract-specific properties that do not generalize to a wide class of smart contracts. There is currently no commonly agreed upon list of properties to use as a starting point in writing a formal specification. We propose three properties that we believe are relevant to all smart contracts: Validity, Liquidity, and Fidelity. Focusing on the concrete case of the Cardano platform, we show how these properties stop exploits similar to the DAO bug, as well as preventing other common issues such as the locking of funds and double satisfaction. We model an account simulation, a multi-signature wallet, and an order book decentralized exchange, as example smart contract specifications using state transition systems in the Agda proof assistant. We formalize the above properties and prove they hold for the models. The models are then separately proven to be functionally equivalent to a validator implementation in Agda, which is translated to Haskell using agda2hs. The Haskell code can then be compiled and put on the Cardano blockchain directly. We use the Cardano Node Emulator to run property-based tests and confirm that our validator works correctly.
Cite as

Tudor Ferariu, Philip Wadler, and Orestis Melkonian. Validity, Liquidity, and Fidelity: Formal Verification for Smart Contracts in Cardano. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ferariu_et_al:OASIcs.FMBC.2025.6,
  author =	{Ferariu, Tudor and Wadler, Philip and Melkonian, Orestis},
  title =	{{Validity, Liquidity, and Fidelity: Formal Verification for Smart Contracts in Cardano}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{6:1--6:21},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.6},
  URN =		{urn:nbn:de:0030-drops-230336},
  doi =		{10.4230/OASIcs.FMBC.2025.6},
  annote =	{Keywords: blockchain, Agda, UTxO, EUTxO, smart contract, formal verification, specification, transition systems, Cardano}
}
Document
DOI: 10.4230/OASIcs.FMBC.2024.10
Structured Contracts in the EUTxO Ledger Model

Authors: Polina Vinogradova, Orestis Melkonian, Philip Wadler, Manuel Chakravarty, Jacco Krijnen, Michael Peyton Jones, James Chapman, and Tudor Ferariu

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract
Blockchain ledgers based on the extended UTxO model support fully expressive smart contracts to specify permissions for performing certain actions, such as spending transaction outputs or minting assets. There have been some attempts to standardize the implementation of stateful programs using this infrastructure, with varying degrees of success. To remedy this, we introduce the framework of structured contracts to formalize what it means for a stateful program to be correctly implemented on the ledger. Using small-step semantics, our approach relates low-level ledger transitions to high-level transitions of the smart contract being specified, thus allowing users to prove that their abstract specification is adequately realized on the blockchain. We argue that the framework is versatile enough to cover a range of examples, in particular proving the equivalence of multiple concrete implementations of the same abstract specification. Building upon prior meta-theoretical results, our results have been mechanized in the Agda proof assistant, paving the way to rigorous verification of smart contracts.
Cite as

Polina Vinogradova, Orestis Melkonian, Philip Wadler, Manuel Chakravarty, Jacco Krijnen, Michael Peyton Jones, James Chapman, and Tudor Ferariu. Structured Contracts in the EUTxO Ledger Model. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{vinogradova_et_al:OASIcs.FMBC.2024.10,
  author =	{Vinogradova, Polina and Melkonian, Orestis and Wadler, Philip and Chakravarty, Manuel and Krijnen, Jacco and Jones, Michael Peyton and Chapman, James and Ferariu, Tudor},
  title =	{{Structured Contracts in the EUTxO Ledger Model}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{10:1--10:19},
  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.10},
  URN =		{urn:nbn:de:0030-drops-198757},
  doi =		{10.4230/OASIcs.FMBC.2024.10},
  annote =	{Keywords: blockchain, ledger, smart contract, formal verification, specification, transition systems, Agda, UTxO, EUTxO, small-step semantics}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact