This document provides the specification of the Byzantine-fault-tolerant (BFT) blockchain consensus protocol QBFT. QBFT provides the following features: - Immediate Finality, - Dynamic Validator Set, - Optimal Byzantine Resilience (the protocol can withstand up to $\lfloor (n-1)/3\rfloor$ Byzantine validators) when operating in a partially synchronous network and - Message complexity of $O(n^2)$, where $n$ is the number of validators. QBFT is based on the BFT agreement protocol presented in [[IBFT-Moniz]].

This Specification is copyright © 2021 Enterprise Ethereum Alliance Incorporated (EEA). It is made available under the terms of the Apache License version 2.0. [[Apache2]]

Unless required by applicable law or agreed to in writing, this specification is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. This is an editors' draft of the QBFT Blockchain Consensus Algorithm Specification version 1, with a number of items still to be addressed, including, but limited to: - Binary encoding of the various messages, - Definition of the algorithm used to determine the validator set in charge of deciding on the block to be appended to a given blockchain and - Formal definition of the systems (networks) where the QBFT protocol can be deployed on. Please send any comments to the EEA Technical Steering Committee at [https://entethalliance.org/contact/](https://entethalliance.org/contact/).

Specification

The specification of QBFT is written using the verification-aware language [[Dafny]] and comprises the following files: [[[#nodedfysec]]], [[[#nodeauxdfysec]]], [[[#typesdfysec]]] and [[[#lemmasdfysec]]]. Overall, the specification is constructed following the [[TLA]]-style approach of using boolean-valued functions (predicates) over old and new states to specify state transition systems, and it uses existential quantifiers to hide the variables that should not appear in the final specification. Specifically, - The type `NodeState` in [[[#typesdfysec]]] models the state of a QBFT node. - The predicate `NodeInit` (defined in [[[#nodedfysec]]]) specifies the set of possible initial states for a QBFT node as follows. The set of all possible initial states for a QBT node with identifier `id` deployed in a system with configuration `c` corresponds the set of all and only those states `s` such that `NodeInit(s, c, id)` evaluates to `true`. - The predicate `NodeNext` (defined in [[[#nodedfysec]]]) specifies how the state of a node should evolve and which messages should be transmitted every time that its local clock ticks. Specifically, if a node's state is `current` and it receives the set of messages `inQbftMessages` at the next tick of its local clock, then the node must transition a state `next` and send messages as specified by a set `outQbftMessages` such that `NodeNext(current, inQbftMessages, next, outQbftMessages)` evaluates to `true`. `outQbftMessages` specifies the set of messages to be sent as follows. Each element `mwr` of `outQbftMessages` indicates that message `mwr.message` is to be sent to node with identifier `mwr.recipient`. - The predicate `IsValidQbftBehaviour``(configuration, id, qbftNodeBehaviour)` (defined in [[[#nodedfysec]]]) provides the actual specification of the QBFT protocol. Specifically, `IsValidQbftBehaviour(configuration, id, qbftNodeBehaviour)` returns `true` if and only if `qbftNodeBehaviour` is an admissible QBFT behaviour for a QBFT node with id `id` deployed in a system with configuration `configuration`. A QBFT behaviour describes the set of QBFT messages sent and the evolution of the blockchain exposed by a node in response to a sequence of input messages. A node complies with the QBFT specification, that is, correctly implements the QBFT specification, only if all of its possible QBFT behaviours are admissible QBFT behaviours. - QBFT behaviours are represented by the type `QbftNodeBehaviour` in [[[#typesdfysec]]] which is constituted by the following components: - the initial blockchain `initialBlockchain` exposed by a QBFT node at the very beginning of the protocol execution and - the infinite sequence of steps `steps` where each step is constituted by - the set of messages received `messagesReceived`, and - the set of messages to be sent `messagesToSend` and the blockchain `newBlockchain` to be exposed by the node after receiving the set of messages `messagesReceived`.

node.dfy

This file is the main corpus of the QBFT specification and it includes the following items: - The definition of the predicate `IsValidQbftBehaviour` which provides the overall specification of the QBFT protocol; - The definition of the predicate `NodeInit` which specifies the set of possible initial states for a QBFT node. - The definition of the predicate `NodeNext` which specifies how the state of a node should evolve and which messages should be transmitted every time that its local clock ticks. `NodeNext` delegates the actual specification of the possible state transitions and message transmissions on the triggering of event *`E`*, where *`E`* can be either the reception of a message or a timer expiry, to the predicate `Upon`*`E`*. - The definitions of the various predicates specifying the possible state transitions and message transmissions for the various events. Link to the file.

node_auxiliary_functions.dfy

This files defines the functions used in [[[#nodedfysec]]]. Link to the file.

types.dfy

This file defines all the types used throughout the specification. Link to the file.

lemmas.dfy

This file does not provide any specification. It just contains lemmas that are used in the `UponCommit` and `UponRoundChange` predicates in [[[#nodedfysec]]] when declaring sets via such-that assignment (`:|`) as the verifier is not able to automatically prove the existence of such sets.

Show the code.
Link to the file.

Additional Information

Defined Terms

The following is a list of terms defined in this Specification.

Acknowledgments

The EEA acknowledges and thanks the many people who contributed to the development of this version of the specification. Please advise us of any errors or omissions. Enterprise Ethereum is built on top of Ethereum, and we are grateful to the entire community who develops Ethereum, for their work and their ongoing collaboration to helps us maintain as much compatibility as possible with the Ethereum ecosystem.