The virtual coupling function based on vehicle communication is currently in the research stage and has not yet formed a standardized file, so it is still difficult to conduct testing experiments on this system. Therefore, formal methods are used to verify the safety and usability of the system model. The virtual coupling train control system is built with the goal of protecting the safe operation of the train, ensuring that the train always runs on the safe part of the track. This article takes the leader car in the formation as the tracking target and establishes a tracking model for the following car. We have developed a hybrid systems model based on the logic of Cyber-Physical Systems (CPS), which includes the discrete part of computer control and follows the continuous differential equations of the physical evolution process in the time domain. The main contribution of this article is to determine the train controller with interval constraints, formally verify the controller with correct safety constraints, formalize the safety of train control in differential dynamic logic, and prove the correctness of the train controller in the theorem prover KeYmaera X.