  We describe an approach to modelling a Byzantine tolerant distributed
algorithm as a family of related finite state machines, generated from a single
meta-model. Various artefacts are generated from each state machine, including
diagrams and source-level protocol implementations. The approach allows a state
machine formulation to be applied to problems for which it would not otherwise
be suitable, increasing confidence in correctness.
