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.