SPIN is a popular open-source software tool, used by thousands of people worldwide, which can be used for the formal verification ofdistributed and concurrent sofware system. the tool was developed at bell labs in the original unix group of the computing sciences research center, starting in 1980. the sofware has been available freely since 1991, and continues to evolve to keep pace with new developments in the field. in this paper, we apply SPIN model checking software to verify the safety and liveness of the transmission control protokol. first, we use SPIN's model specification language pomela to model the the transmission control protokol, and than we use the SPIN and its graphical user interface Xspin to verity the properties of the transmissioncontrol protokol. we will describe the model checking process, the tools used, and the methods and conditions necessary to successfully perform model checking pn the transmission control protocol.