# Aleobft

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 static contains
a formal specification and correctness proofs
of a version of AleoBFT with static committees and without stake,
which is therefore similar to Bullshark,
but with some differences unique to AleoBFT.
We have also started another directory dynamic,
for a version of AleoBFT with dynamic committees.
We plan to add other subdirectories,
parallel to static and dynamic,
for versions of the formal specification and correctness proofs
that cover additional aspects of AleoBFT,
such as stake and syncing.
While this work is in progress,
we may have these multiple subdirectories for different versions,
but eventually we may converge to one version,
in this directory (not in any subdirectory),
which subsumes all the previous versions.
The overall reason for tackling increasingly complex versions
of the formal specification and correctness proofs of AleoBFT
is to better manage the inherent complexity of the protocol.

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.

### Subtopics

- Aleobft-static
- Formal specification and correctness proofs of
AleoBFT with static committees.
- Aleobft-dynamic
- Formal specification and correctness proofs of
AleoBFT with dynamic committees.
- Library-extensions
- Library extensions.