PRISM est un outil open source dédié à la vérification formelle de systèmes probabilistes et stochastiques. Il permet de modéliser et d'analyser des systèmes complexes comme les protocoles de communication, les algorithmes distribués ou les réseaux de files d'attente. L'outil prend en charge plusieurs formalismes (DTMC, CTMC, MDP, etc.) et offre des fonctionnalités avancées pour l'évaluation de propriétés quantitatives et temporelles.