As distributed, communication-based protection systems become more prevalent in the emerging smart grid, the task of critically assessing their reliability has become increasingly challenging due to the complexity of their underlying software designs. This paper demonstrates that the discipline of software model checking can be applied to smart grid protection software designs to rigorously assess their fault tolerance. In this paper, the SPIN model checker is applied to a published wide-area backup protection system (WABPS). The WABPS was specifically architected to be highly reliable under various kinds of common failure scenarios, including mechanical malfunctions, erroneous sensor readings, and communication failures. However, because of its built-in redundancy and decentralized peer-to-peer design, calculating its precise fault tolerance is nontrivial. This paper shows how SPIN can be applied to the WABPS's design to brute-force prove the limits of the number and types of failures that can occur while the system remains able to successfully perform its function. This same technique is applicable to a wide variety of smart grid protection software designs, and the information it provides is invaluable to protection engineers during the development of new systems, for assessing the quality of competing designs, and for risk management purposes.