Search Results

Documents authored by Jaskelioff, Mauro

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.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}
}
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