AleoBFT is the Byzantine-fault-tolerant (BFT) consensus protocol of the Aleo blockchain, implemented in snarkOS (mostly) and in snarkVM (for some functionality). AleoBFT is based on Narwhal and Bullshark, with extensions for dynamic committees with staking. As part of our ongoing effort to apply formal verification techniques to AleoBFT, we’re excited to announce the completion of a major milestone: we now have a formal model of AleoBFT with dynamic committees, and a formal proof that, in that model, blockchains of different validators never fork, i.e. all validators commit to the same data. This result goes beyond the analogous properties of Bullshark, which has static committees; dynamic committees are a significant extension, whose correctness is not obvious at first sight.
But why does this actually matter? And what’s next?
A quick recap: what are BFT consensus protocols
BFT consensus protocols aim to ensure that a network of validators reaches consensus on state, assuming a sufficient number of validators correctly follow the protocol. For example, in Bullshark, out of n = 3f+1 total validators, as long as at least 2f+1 validators behave correctly, a number of desired properties holds, such as the non-forking of blockchains.
One of the subtle aspects we learned in the course of our formal verification work is that the aforementioned 2f+1 bound critically depends on the assumption that n has the form 3f+1. However, this is not a fully general assumption, because in a practical system n may not always have that form, the other two possibilities being 3f+2 and 3f+3. For a general number n of validators, the correct minimum number of correct validators is n-f, where f is the maximum integer strictly less than n/3.
The necessity of dynamic committees
The original Bullshark construction was designed with static committees in mind. However, intuitively, that doesn’t sound very realistic. Organizations and societies change, and if we expect the same entities to be responsible for maintaining the integrity of a cryptocurrency network forever, that is a recipe for failure. One way out is to periodically make use of a trusted coordinator, or to rely on the benevolence of the network’s community, to decide on a “transition of power” and to determine new validators. However, once that becomes a relied-upon process, we lose out on the true magic of distributed consensus algorithms. A more flexible solution is to build into the protocol the ability to change the validators dynamically.
If you look at other popular consensus algorithms, such as Bitcoin’s Proof of Work, Chia’s Proofs of Space and Time, or Ethereum’s Proof of Stake, dynamic validator sets are the name of the game. And with that in mind, AleoBFT was born, a consensus algorithm giving strong consistency guarantees while having support for dynamic committee changes.
In AleoBFT, a committee consists of one or more validators, each with a certain amount of stake; during the execution of the protocol, certain decisions depend on that stake. Starting with a known genesis committee when the Aleo mainnet launched, validators bond and unbond via specific kinds of transactions, intermixed with the other kinds, all committed to the blockchain. This makes AleoBFT committees very dynamic, potentially changeable at every block, where a new block may be produced every two rounds of the protocol. Since validators do not commit all the blocks at the same time (they may be ahead or behind relative to each other), it would be difficult, or cause intolerable delays, for validators to always agree on the committee resulting from the latest block, and use that to reach consensus at the next round. Thus, AleoBFT uses an innovative lookback approach, by which the committee in charge of the next round is the one resulting not from the previous block, but from a fixed number of rounds in the past (currently 100). In other words, there is a “delay” (of 100 rounds) between the bonding or unbonding of a validator and its starting or ending participation in achieving consensus. (This explanation of lookback and dynamic committees is slightly simplified for brevity, but gives the general idea.)
The ACL2 formalization
Our formal model and proofs of AleoBFT are written in the ACL2 theorem prover; they are available as part of the GitHub repository of ACL2 and its libraries, precisely at this location. We formally modeled AleoBFT as a labeled state transition system, whose state consists of the validators and the network that connects them, and whose transitions describe changes to the validators’ internal states and to the network, the latter in the form of messages exchanged among the validators. We formally proved the non-forking of blockchains via a number of invariants on the reachable states of the system. These invariants are complex, and several of them are interdependent: in particular, the agreement (i.e. non-forking) of the blockchains depends on the non-equivocation of the partially ordered certificates from which the blockchain is totally ordered, the non-equivocation of those certificates depends on the validators agreeing on the committees in charge of the rounds of those certificates, and the committees are calculated from the blockchains, which must be therefore agreed upon. Our top-level induction proof ensures that these interdependencies are inductively well-formed, and that there is no circular reasoning.
This approach has given us assurance that it is perfectly allowed for the committee to change entirely at a certain round/block: the protocol still works correctly, so long as the right committees are used for the right things at each round (signers, voters, and predecessors), which is quite remarkable.
Some obligatory fine print
As in all uses of formal verification, it is important to emphasize what has been and has not been formally proved. We have formally proved non-forking in our formal model of AleoBFT, which we have built based on careful examination of the AleoBFT implementation in snarkOS and snarkVM. We have not formally proved the correctness of snarkOS and snarkVM. Even so, a formal proof of a model of snarkOS and snarkVM provides dramatically higher assurance than just testing and informal reasoning.
From lookback committees to looking ahead
We will be continuing our formal verification efforts in various directions. An immediate direction is to generalize our model and proofs from using numbers of validators as n and f, to stake associated to validators. We also plan to formally study additional properties of AleoBFT, in particular related to liveness.
We are writing an academic paper describing our formal model and proofs of blockchain non-forking. We welcome you to keep track of our work, ask questions, and dare we say, collaborate with us to help make modern consensus implementations more and more robust.