This document attempts to explain Roberto's QBFT Dafny specification. Dafny is a programming language used for formal verification of algorithms. It can verify correctness, termination property and that there are no runtime errors.
The code follows a state machine transition
design, using logic programming
predicates
that validate the transition rules of the system.
There is a Blockchain
entity which, basically, is comprised of a sequence of blocks. The Blockchain has nodes
, out of which some are validators
. The validators run QBFT
as the consensus mechanism of the blockchain, adding a block
, with incremental height
, each time the consensus terminates.
The node has a state
. The transition rule is the predicate NodeNext that verifies the transition:
flowchart LR
s1("(Current State, list of incoming messages)")
s2("(Next State, list of output messages)")
s1-->s2
The NodeNext predicate is supposed to be called upon a clock tick, the period of which the messages are also considered transmitted and processed.
- Types
- Auxiliary functions
- Node (main file)
- Lemmas (helper file)