This study focuses on the formal verification of a spacecraft attitude control system, essential for ensuring the safety and efficacy of spacecraft operations. The paper discusses the challenges in verifying spacecraft control systems due to their nonlinear and high-dimensional nature. Formal verification methods, particularly reachable set analysis, are highlighted for their effectiveness in verifying complex dynamic systems. The research emphasizes the applicability of the methodology to other dynamic systems for safety verification. The spacecraft dynamic system is detailed, showcasing controllers designed based on Lyapunov stability theory for attitude control using reaction wheels. Through formal verification methods, particularly using the CORA toolbox in Matlab, the study analyzes the safety and performance of traditional proportional-differential controller. Experimental results demonstrate the application of formal verification in assessing the safety of spacecraft control systems, with a focus on satisfaction reaction wheel angular velocities and spacecraft angular velocities constrains. The study concludes by discussing the implications of the verification results and the potential for integrating formal verification methods in spacecraft design and operation.