|
|
|---|
|
|
|
|---|
Formal specification and correctness proofs of AleoBFT with dynamic committees with stake and proposals.
We define a formal model of an abstraction of the AleoBFT protocol that captures both the Narwhal and the Bullshark aspects of the protocol, but with dynamic committees and with stake, which are a significant extensions. This model does not capture garbage collection or syncing.
This is work in progress: the definition of the system is complete, but the correctness proofs are not here yet.