A Process Calculus for Formally Verifying Blockchain Consensus Protocols

TL;DR

This paper introduces the $ atural$-calculus, a process calculus designed for formal verification of blockchain consensus protocols, featuring a unique operational semantics with layered transition systems.

Contribution

It presents the $ atural$-calculus, a novel domain-specific language with a modular semantics framework for verifying blockchain consensus protocols.

Findings

Defines the $ atural$-calculus language and semantics

Introduces layered transition systems for data transfer and scope management

Provides a generic algebraic framework for concurrency concepts

Abstract

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 $\natural$-calculus (pronounced "natural calculus"), a general-purpose process calculus that serves as our implementation language. The $\natural$-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 $\natural$-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.