|
|
|---|
|
|
|
|---|
Formal specification 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 with staking. AleoBFT is implemented in snarkOS (primarily) and snarkVM (for some functionality).
This directory contains works in progress towards
a formal specification and correctness proofs of AleoBFT.
The subdirectory
We formally specify AleoBFT as a labeled state transition system: we define the possible states of the system (of all validators), the possible events that can take place in the system, and then we define, in essence, a ternary transition relation each of whose triples relates an old state, an event, and a new state; the events are the labels in this labeled state transition system. In general, not every event may happen in every state, which is reflected in the transition relation not having triples with those given old states and events. More precisely, we define our transition relation via a predicate and a function: the predicate says whether an event is possible in a state; the function says, for the events and states for which the predicate holds, what the new state is after the event. In general there are multiple possible events in every state, which makes the system nondeterministic; however, given one of these events, the next state is determined by old state and event (we achieve that by putting enough information in the event).
We formulate the correctness properties of AleoBFT mainly as state invariants, which we show to hold in the initial states and to be preserved by state transitions.