PBFT is a byzantine fault tolerant consensus protocol used to realise a replicated state machine ¹. The specification for it is in progress and can be found here.

I will shortly be adding a section on how we can traverse all behaviours in which byzantine behaviour can occur to verify that the algorithm indeed maintains safety in all of them.