This study focuses on verifying correctness and completeness of Fault Tree Analysis (FTA) for Safety Integrity Level (SIL). The methods to evaluate SIL are risk graph, FTA, ETA (Event Tree Analysis), and LOPA (Layer of Protection Analysis). Among these methods, FTA is being used frequently as a quantitative method because fault tree shows the cause-consequence of the Safety Instrumented System (SIS). Whereas FTA largely depends on domain-specific knowledge of human experts, it lacks formality and the evaluating process is manual. Therefore we propose a novel approach which automatically proves the correctness and completeness of fault trees based on a formal model by model checking. We also define consistency conditions in Computational Tree Logic (CTL), a widely used input language for model checkers. The idea of the verification of FTA is to formally specify the system model and to prove correctness and completeness of FTA. This paper presents how model checking approach using CTL can be used efficiently in the verification of FTA for SIL through case studies. A failure in the safety instrumented system could result in the reduction of plant efficiency and availability as well as in the occurrence of safety critical situations. The use of SIS enhances flexibility providing potential benefits, and it also decreases risks from random failures and design errors. The request for safety assessment and validation of SIS is becoming more important. This increasing demand has led to the definition of an emerging standard (IEC 61508) that provides general guidelines and rules without addressing any specific technological sector. The international standard IEC 61508 has been widely accepted as the basis for specification, design, and operational of SIS. The standard sets out a risk-based approach for deciding the SIL for systems performing safety functions. The determination of the appropriate SIL is based on the concept of risk and IEC 61508 and 61511 provide a number qualitative and quantitative method. Determining SIL depends on the calculation of Probability of Failure on Demand (PFD) or dangerous failures per year. The calculations depend on the choice of technology, mode of operation (low or high-demand), architecture, diagnostics, systematic failures, test interval and maintenance. Various techniques can be used to determine PFD for a low-demand operation and the probability of dangerous failures for high-demand or continuous mode operation. The quantitative techniques used for the safety integrity level as many such as reliability block diagram, simplified equations, fault tree analysis and Markov modeling. Among these methods, FTA is being used plentifully as a quantitative method because fault tree symbols are used to show the failure logic of the SIS. The FTA technique is based on the assumption that components have a binary behavior (up and down) and that component failures are statistically independent. The graphical nature of this technique affords visualization of failure paths. Fault trees (FT) can model diverse technologies and complex failure. Whereas FTA largely depends on domain-specific knowledge of human experts, it lacks formality and the process is not automated. Moreover, it does not adapt the FT notation to represent temporal relationship between faults and event in dynamic systems. In order to solve these problems, we attempt to verifying correctness and completeness of FTA for SIL. The idea of the verification of FTA is to formally specify the system model and to prove correctness and completeness of FTA. For verifying formal FTA we have to i) formally specify the system, ii) develop fault trees for the main system hazards, iii) formalize the fault tree events, and iv) verify the proof conditions for every gate. The idea of the integration of FTA and formal methods is to formally specify the system model and to prove correctness and completeness of FTA. Therefore, the FTA has to be formalized. We define a semantics of fault trees which consists of proof conditions for every gate in the tree. We assign so called correctness and completeness conditions to the gates. The correctness condition guarantees that the noted sub-events actually lead to the top event. The completeness condition guarantees that only the sub-events lead to the top event, i.e. no cause was overlooked during the FTA. If every proof condition is verified, the correctness and completeness of the fault tree is guaranteed, i.e. the basic events are necessary for causing the system level hazard and only the basic events can cause the hazard. This study focuses on verifying correctness and completeness of Fault Tree Analysis (FTA) for Safety Integrity Level (SIL). The benefits of this study are that it provides the possibility of formally validating FTA by proving correctness and completeness of the fault trees. In additional to this benefit, it is possible that the CTL technique proves the FTA based SIL.