Search Results

Documents authored by Melkonian, Orestis

Artifact
Software
DOI: 10.4230/artifacts.23004
omelkonian/hoare-ledgers

Authors: Orestis Melkonian

Abstract
Cite as

Orestis Melkonian. omelkonian/hoare-ledgers (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23004,
   title = {{omelkonian/hoare-ledgers}}, 
   author = {Melkonian, Orestis},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:fe2bce9b8779645c5a992156ea43604432ccc496}{\texttt{swh:1:dir:fe2bce9b8779645c5a992156ea43604432ccc496}} (visited on 2025-05-16)},
   url = {https://github.com/omelkonian/hoare-ledgers},
   doi = {10.4230/artifacts.23004},
}
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},
}
Artifact
Software
DOI: 10.4230/artifacts.23005
input-output-hk/formal-streamlet

Authors: Orestis Melkonian and Mauro Jaskelioff

Abstract
Cite as

Orestis Melkonian, Mauro Jaskelioff. input-output-hk/formal-streamlet (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23005,
   title = {{input-output-hk/formal-streamlet}}, 
   author = {Melkonian, Orestis and Jaskelioff, Mauro},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:70b9f1e274a05bad6f0e9fd5fe4e0f70033f503f}{\texttt{swh:1:dir:70b9f1e274a05bad6f0e9fd5fe4e0f70033f503f}} (visited on 2025-05-16)},
   url = {https://github.com/input-output-hk/formal-streamlet},
   doi = {10.4230/artifacts.23005},
}
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.2025.7
A Readable and Computable Formalization of the Streamlet Consensus Protocol

Authors: Mauro Jaskelioff, Orestis Melkonian, and James Chapman

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

Abstract
Consensus protocols are the fundamental building block of blockchain technology. Hence, correctness of the consensus protocol is essential for the construction of a reliable system. In the past few years, we saw the introduction of a myriad of new protocols of the BFT family of consensus protocols. The Streamlet protocol is one of these new protocols, which while not the fastest, it is certainly the simplest one. In order to have strong guarantees for the protocol and its implementations we want to obtain formalizations that are readable enough to be used to communicate between formalizers and implementors, that have a mechanized proof of correctness and that can support the testing of implementations. We present a readable and computable formalization of the Streamlet protocol in Agda, provide a mechanization of its proof of consistency, and show how one may use the formalization for testing implementations of it.
Cite as

Mauro Jaskelioff, Orestis Melkonian, and James Chapman. A Readable and Computable Formalization of the Streamlet Consensus Protocol. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jaskelioff_et_al:OASIcs.FMBC.2025.7,
  author =	{Jaskelioff, Mauro and Melkonian, Orestis and Chapman, James},
  title =	{{A Readable and Computable Formalization of the Streamlet Consensus Protocol}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{7:1--7:18},
  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.7},
  URN =		{urn:nbn:de:0030-drops-230356},
  doi =		{10.4230/OASIcs.FMBC.2025.7},
  annote =	{Keywords: blockchain, Streamlet, consensus, formal verification, Agda}
}
Document
DOI: 10.4230/OASIcs.FMBC.2025.10
Program Logics for Ledgers

Authors: Orestis Melkonian, Wouter Swierstra, and James Chapman

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

Abstract
Distributed ledgers nowadays manage substantial monetary funds in the form of cryptocurrencies such as Bitcoin, Ethereum, and Cardano. For such ledgers to be safe, operations that add new entries must be cryptographically sound - but it is less clear how to reason effectively about such ever-growing linear data structures. This paper demonstrates how distributed ledgers may be viewed as computer programs, that, when executed, transfer funds between various parties. As a result, familiar program logics, such as Hoare logic, are applied in a novel setting. Borrowing ideas from concurrent separation logic, this enables modular reasoning principles over arbitrary fragments of any ledger. All of our results have been mechanised in the Agda proof assistant.
Cite as

Orestis Melkonian, Wouter Swierstra, and James Chapman. Program Logics for Ledgers. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{melkonian_et_al:OASIcs.FMBC.2025.10,
  author =	{Melkonian, Orestis and Swierstra, Wouter and Chapman, James},
  title =	{{Program Logics for Ledgers}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{10:1--10:22},
  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.10},
  URN =		{urn:nbn:de:0030-drops-230370},
  doi =		{10.4230/OASIcs.FMBC.2025.10},
  annote =	{Keywords: blockchain, distributed ledgers, UTxO separation logic, program semantics, formal verification, Agda}
}
Artifact
Software
DOI: 10.4230/artifacts.22485
IntersectMBO/formal-ledger-specifications

Authors: Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell

Abstract
Cite as

Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, Ulf Norell. IntersectMBO/formal-ledger-specifications (Software, Agda Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22485,
   title = {{IntersectMBO/formal-ledger-specifications}}, 
   author = {Knispel, Andre and Melkonian, Orestis and Chapman, James and Hill, Alasdair and J\"{a}\"{a}ger, Joosep and DeMeo, William and Norell, Ulf},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:085aefb014706c3ee4bcf1a9f85fcceaf10ba4cc;origin=https://github.com/IntersectMBO/formal-ledger-specifications;visit=swh:1:snp:5097bdc07a9030f7e251cb6529989d442bb82f35;anchor=swh:1:rev:002b7226a3af8e5e1068fd0c8fd1fcbb51bba64e}{\texttt{swh:1:dir:085aefb014706c3ee4bcf1a9f85fcceaf10ba4cc}} (visited on 2024-11-28)},
   url = {https://github.com/IntersectMBO/formal-ledger-specifications},
   doi = {10.4230/artifacts.22485},
}
Document
DOI: 10.4230/OASIcs.FMBC.2024.2
Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda

Authors: Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell

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

Abstract
Blockchain systems comprise critical software that handle substantial monetary funds, rendering them excellent candidates for formal verification. One of their core components is the underlying ledger that does all the accounting: keeping track of transactions and their validity, etc. Unfortunately, previous theoretical studies are typically confined to an idealized setting, while specifications for real implementations are scarce; either the functionality is directly implemented without a proper specification, or at best an informal specification is written on paper. The present work expands beyond prior meta-theoretical investigations of the EUTxO model to encompass the full scale of the Cardano blockchain: our formal specification describes a hierarchy of modular transitions that covers all the intricacies of a realistic blockchain, such as fully expressive smart contracts and decentralized governance. It is mechanized in a proof assistant, thus enjoys a higher standard of rigor: type-checking prevents minor oversights that were frequent in previous informal approaches; key meta-theoretical properties can now be formally proven; it is an executable specification against which the implementation in production is being tested for conformance; and it provides firm foundations for smart contract verification. Apart from a safety net to keep us in check, the formalization also provides a guideline for the ledger design: one informs the other in a symbiotic way, especially in the case of state-of-the-art features like decentralized governance, which is an emerging sub-field of blockchain research that however mandates a more exploratory approach. All the results presented in this paper have been mechanized in the Agda proof assistant and are publicly available. In fact, this document is itself a literate Agda script and all rendered code has been successfully type-checked.
Cite as

Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell. Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@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}
}
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}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.4
Reconciling Event Structures with Modern Multiprocessors (Artifact)

Authors: Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
The artifact is a virtual machine image containing two Coq packages which include mechanization of proofs stated in the paper. The first package imm contains a modified version of the Intermediate Memory Model, extended with the support of sequentially consistent atomics, and the compilation correctness proofs from it to hardware models. The second package weakestmoToImm contains a definition of the Weakestmo memory model as well as a compilation correctness proof from it to IMM.
Cite as

Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis. Reconciling Event Structures with Modern Multiprocessors (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{moiseenko_et_al:DARTS.6.2.4,
  author =	{Moiseenko, Evgenii and Podkopaev, Anton and Lahav, Ori and Melkonian, Orestis and Vafeiadis, Viktor},
  title =	{{Reconciling Event Structures with Modern Multiprocessors (Artifact)}},
  pages =	{4:1--4:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Moiseenko, Evgenii and Podkopaev, Anton and Lahav, Ori and Melkonian, Orestis and Vafeiadis, Viktor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.4},
  URN =		{urn:nbn:de:0030-drops-132015},
  doi =		{10.4230/DARTS.6.2.4},
  annote =	{Keywords: Weak Memory Consistency, Event Structures, IMM, Weakestmo}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.5
Reconciling Event Structures with Modern Multiprocessors

Authors: Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Weakestmo is a recently proposed memory consistency model that uses event structures to resolve the infamous "out-of-thin-air" problem and to enable efficient compilation to hardware. Nevertheless, this latter property - compilation correctness - has not yet been formally established. This paper closes this gap by establishing correctness of the intended compilation schemes from Weakestmo to a wide range of formal hardware memory models (x86, POWER, ARMv7, ARMv8) in the Coq proof assistant. Our proof is the first that establishes correctness of compilation of an event-structure-based model that forbids "out-of-thin-air" behaviors, as well as the first mechanized compilation proof of a weak memory model supporting sequentially consistent accesses to such a range of hardware platforms. Our compilation proof goes via the recent Intermediate Memory Model (IMM), which we suitably extend with sequentially consistent accesses.
Cite as

Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis. Reconciling Event Structures with Modern Multiprocessors. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 5:1-5:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{moiseenko_et_al:LIPIcs.ECOOP.2020.5,
  author =	{Moiseenko, Evgenii and Podkopaev, Anton and Lahav, Ori and Melkonian, Orestis and Vafeiadis, Viktor},
  title =	{{Reconciling Event Structures with Modern Multiprocessors}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{5:1--5:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.5},
  URN =		{urn:nbn:de:0030-drops-131622},
  doi =		{10.4230/LIPIcs.ECOOP.2020.5},
  annote =	{Keywords: Weak Memory Consistency, Event Structures, IMM, Weakestmo}
}
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