Probabilistic and statistical analysis is a tool of fundamental importance to virtually all scientists and engineers as they often have to deal with systems that exhibit random or unpredictable elements. Traditionally, computer simulation techniques are used to perform probabilistic analysis. However, they provide less accurate results and cannot handle large-scale problems due to their enormous computer processing time requirements. To overcome these limitations, we propose to perform formal probabilistic and statistical analysis using higher-order logic theorem proving. We provide a framework for the formalization of both discrete and continuous random variables and the ability to formally verify system's probabilistic and statistical properties. The analysis carried out in this way is free from any approximation or precision issues due to the mathematical nature of the models and the inherent soundness of the theorem proving approach. In order to illustrate the practical effectiveness of the proposed framework, we present the probabilistic analysis of four examples across three application areas: the Coupon Collector's problem (software), the Stop-and-Wait protocol (telecommunications), the reliability of memory arrays (microelectronics), and floating-point error analysis (computer hardware).