Fault Tree Analysis is a traditional deductive safety analysis technique that is applied during the system design stage. However, traditional fault trees often suffer from a lack of formal semantics to check the correctness or consistency of the descriptions. To overcome this limitation, we first propose a novel formal fault tree construction model in which the correctness of the fault tree is proved by the construction process per se, while at the same time subtler and more precise system safety properties are discovered. Then, based on analyzing the results of our formal fault tree model, we demonstrate how CafeOBJ, a wide spectrum specification language based on multiple logical foundations, can be used to formally model, specify, and verify a system as well as its important safety properties. Thus, we propose an integrated system analysis platform that will enable engineers to find, analyze, and solve problems more efficiently and effectively.