Abstract: This paper formalizes the probability theory in Isabelle/HOL/Isar based on the mathematical measure theory. It presents the formal definition of probability space in Isabelle/HOL and verifies the main properties of probability measure. Formally it verifies the Caratheodory’s extension theorem, which lays a foundation for the construction of various probability spaces. This formalization will facilitate the formal verification of probabilistic algorithms and probabilistic systems in Isabelle/HOL.

Key words: probability space, Caratheodory’s extension theorem, formal verification, Isabelle/HOL/Isar