Abstract. This paper gives a brief overview of version 2.0 of PRISM, a tool for the automatic formal verification of probabilistic systems, and some of the case studies to which it has already been applied.