Abstract: The Interlocking System is a safety critical system. Its safety cannot be guaranteed only by testing. Formal verification can be used to verify the consistency between the applied logic and the safety requirements of the System. In this article, the general safety requirements were instantiated with the specific station layout. Then the specific safety requirements were verified through inputting them to the SAT induction constraint solver. The completeness of the method was guaranteed by covering all the instances, all the cycles and all the state space of each cycle.