|
|
|---|
|
|
|
|---|
Formal specification and correctness proofs of AleoBFT with dynamic committees with stake.
We define a formal model of an abstraction of the AleoBFT protocol 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 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.