|
|
|---|
|
|
|
|---|
Formal model and correctness proofs of AleoBFT.
AleoBFT is the consensus protocol of the Aleo blockchain. AleoBFT is based on Narwhal and Bullshark, particuarly partially synchronous Bullshark, which AleoBFT extends with dynamic committees, staking, and syncing. AleoBFT is implemented in snarkOS (primarily) and snarkVM (for some functionality).
This directory contains a formal model and correctness proofs of AleoBFT. The model is an abstraction of AleoBFT that mainly captures the Bullshark aspects of the protocol, but with dynamic committees and with stake, which are significant extensions to Bullshark. The Narwhal aspects of AleoBFT are modeled only at an abstract level, similarly to the way that the Bullshark papers model the underlying DAG consensus layer. The level of abstraction of this model is about the same as the Bullshark papers. This model does not capture garbage collection or syncing.
The subdirectory
The proofs of correctness in both the current and next version mainly concern the safety property that blockchains do not fork. Proving other correctness properties is future work.
The current version of the model and proofs is
the last one of a series of versions that we have developed.
We started with a version with static committees without stake,
which was therefore very similar to plain Bullshark.
Then we made the significant extension to dynamic committees,
initially without stake, and then with stake;
adding stake was not a big extension.
The
The current version essentially corresponds to the contents of this arXiv paper, but the current version has undergone some improvements since the paper was written.