DROPS

Artifact

Software

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

Search Results

Documents authored by Jaskelioff, Mauro

input-output-hk/formal-streamlet

Abstract

Cite as

A Readable and Computable Formalization of the Streamlet Consensus Protocol

Abstract

Cite as

Thanks for your feedback!

Could not send message