RoboChart is a UML-like language designed for modelling autonomous and mobile robots. It includes timed and probabilistic primitives. In this chapter, we discuss first why we need probability by surveying how we use it in designing robots. To illustrate our approach, we focus on the verification of probabilistic robotic algorithms for pose estimation. We verify a model-fitting algorithm: random sample consensus (Ransac). This is a popular algorithm, representative of a class of particle-filter algorithms. We analyse the aspects of the algorithm and show how to model-check properties and how to get stronger guarantees using a program logic. Our contributions are a survey of probabilistic robotic applications and an approach to verifying probabilistic algorithms developed using RoboStar technology.