XYZ/E is used to specify and verify the triple-modular redundancy fault-tolerant system. Assuming that each computer is loaded with a determined sequential program P which continuously outputs data to the outer environment, the case P running on single processor is illustrated by an XYZ/E program SingleProcess_P, and the property of program P is specified by a temporal logical formula Spec_P. Finally, it is proved that the program TripleProcessors_P obtained from the triple-modular redundancy way can still satisfy Spec_P in spite of hardware errors.