In most applications using genetic programming (GP), objective functions are obtained by a terminating calculation. However, the terminating calculation cannot evaluate distributed fault-tolerant programs accurately. A key distinction in synthesizing distributed fault-tolerant programs is that they are inherently non-deterministic, potentially having infinite computations and executing in an unpredictable environment. In this study, we apply a model checking technique - Binary Decision Diagrams (BDDs) - to GP, evaluating distributed programs by computing reachable states of the given program and identifying whether it satisfies its specification. We present scenario-based multi-objective approach that each program is evaluated under different scenarios which represent various environments. The computation of the programs are considered in two different semantics respectively: interleaving and maximum-parallelism. In the end, we illustrate our approach with a Byzantine agreement problem, a token ring problem and a consensus protocol using failure detector S. For the first time, this work automatically synthesizes the consensus protocol with S. The results show the proposed method enhances the effectiveness of GP in all studied cases when using maximum-parallelism semantic.