Hybrid System is a very important subclass of real time embedded system. The behavior of hybrid system is tangled with discrete control mode transformation and continuous real time behavior, therefore very complex and difficult to control. As hybrid system is widely used in safety-critical areas like industry, defense and transportation system, it is very important to analyze and understand the system effectively to guarantee the safe operation of the system. Ordinary techniques like testing and simulation can only observe the behavior of the system under given input. As they cannot exhaust all the possible inputs and scenarios, they are not enough to guarantee the safety of the system. In contrast to testing based techniques, formal method can answer questions like if the system will never violate certain specification by traversing the complete state space of the system. Therefore, it is very important to pursue the direction of formal verification of safety-critical hybrid system. Formal method consists of formal specification and formal verification. This paper reviews the modeling language and specification of hybrid system as well as techniques in model checking and theorem proving. In addition, it discusses the potential future directions in the related area.