Blockchains are becoming increasingly relevant in a variety of fields, such as finance, logistics, and real estate. The fundamental task of a blockchain system is to establish data consistency among distributed agents in an open network. Blockchain consensus protocols are central for performing this task. Since consensus protocols play such a crucial role in blockchain technology, several projects are underway that apply formal methods to these protocols. One such project is carried out by a team of the Formal Methods Group at IOHK. This project, in which the author is involved, aims at a formally verified implementation of the Ouroboros family of consensus protocols, the backbone of the Cardano blockchain. The first outcome of our project is the -calculus (pronounced “natural calculus”), a general-purpose process calculus that serves as our implementation language. The (formula presented)-calculus is a domain-specific language embedded in a functional host language using higher-order abstract syntax. This paper will be a ramble through the (formula presented)-calculus. First we will look at its language and its operational semantics. The latter is unique in that it uses a stack of two labeled transition systems to treat phenomena like data transfer and the opening and closing of channel scope in a modular fashion. The presence of multiple transition systems calls for a generic treatment of derived concurrency concepts. We will see how such a treatment can be achieved by capturing notions like scope opening and silent transitions abstractly using axiomatically defined algebraic structures based on functors and monads.
CITATION STYLE
Jeltsch, W. (2020). A Process Calculus for Formally Verifying Blockchain Consensus Protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12057 LNAI, pp. 24–39). Springer. https://doi.org/10.1007/978-3-030-46714-2_2
Mendeley helps you to discover research relevant for your work.