PRISM is a probabilistic model checker, a formal verification software tool for the modelling and analysis of systems that exhibit probabilistic behaviour. PRISM was introduced around 2002 in the context of Parker's PhD work and is still under active development.