Transactions.
Validators propose transactions for inclusion in the blockchain. Transactions have a rich structure. In fact, AleoBFT handles not only transactions, but also `solutions' and (possibly in the future) `ratifications', which together with transactions form `transmissions'.
However, most of these details are unimportant for our model. Our model sticks to the more common term `transaction', which can be thought as modeling also the other kinds of transmissions. Our model is concerned with two kinds of transactions: one to bond a validator (i.e. add the validator to the committee with some stake), and one to unbond a validator (i.e. remove the validator from the committee). So we consider these two kinds of transactions, plus an opaque one for all other kinds of transactions.