NeoResearch recently announced its intent to produce formal correctness proofs for dBFT, the consensus mechanism used by the Neo blockchain. This process is facilitated through the development of mathematical models that can be used to predict failures and attacks related to consensus. The models under development for each version of dBFT can be found here.

Building on work started last year, NeoResearch used its model to prove the single block forks that occurred in the first version of dBFT. Known colloquially as sporks in the Neo community, these single block forks could happen if a consensus node acting as speaker managed to gather enough signatures to validate its block but failed to broadcast it to the network before the round timeout.

Other nodes would begin a new round of consensus to produce a new block at the same block height, however the original block could also be broadcast. Both blocks would share the same height as in conventional blockchain forks, however the original block would be immediately orphaned as it would not be accepted by other consensus nodes. Despite this, since they would still be considered valid by P2P nodes, some nodes could accept it the orphaned block and become stuck, unable to follow further consensus rounds until manually reset.

Successfully proving the occurrence of sporks via the mathematical model lends credibility to its accuracy, helping ensure that it is a dependable tool for testing potential modifications or extensions to dBFT moving forward. The constraints used in the model for dBFT 1.0 can be found here.

NeoResearch members are currently adapting the model to work with dBFT 2.0, an improved version of the protocol with a third consensus phase designed to prevent sporks. Once the model is appropriately adjusted for 2.0, NeoResearch plans to use it to guide the next iteration of dBFT’s development.

The team’s findings are expected to be included as part of a formal report on dBFT, which discusses its history and potential directions for improvement in the 3.0 version. A prerelease version of this report has already been shared with the community, which highlights some of the potential changes.

The third version of dBFT is intended to further improve the reliability of Neo’s consensus by preventing block generation delays. Two possible approaches have been highlighted; dBFT could follow in the footsteps of fully asynchronous BFT mechanisms such as HoneyBadger, or begin using redundant speaker nodes to propose blocks simultaneously.

Additionally, consideration is being given to mechanisms that could help increase decentralization by improving network participation. Avenues being researched for this purpose include allowing the creation of community-operated “guest nodes” with a sufficient stake, alongside incentivization improvements being pursued as part of changes to the Neo3 governance model.