Realistic analysis of many systems requires availability of accurate methods and tools. Formal methods such as model checking and theorem proving have seen intereset in attempting problems involving modeling of random phenomenon and random behavior of complex systems. In our research, we focus on the formalization of basic underlying mathematics essential for reasoning about probabilities, random variables, markov chains, reliability and Information theory. We develop methedologies and tools for application to engineering problems. Following are three main active projects in our group at this time.