In recent years, with the rapid development of artificial intelligence, people encounter more and more robots, such as soccer robots, unmanned aerial vehicles, and unmanned automobiles in their daily life. How to guarantee the safety with those autonomous robots, especially team of robots on the move, has drawn people's attention. Hybrid CSP (HCSP) is a modelling language for hybrid systems. As an extension of CSP, HCSP introduces into CSP differential equations to describe the continuous behavior and control logic in hybrid systems. It can be used to model large-scale control systems, especially those with occurrences of communication events. In this paper, the trajectory planning algorithm is first modeled for multi robots using HCSP, and some properties are then formally proved with the theorem prover HProver. The paper finally proves that collision will never happen during the whole process under some initial conditions.