Presenting joint work with Alessio Lomuscio, which has been published at AAMAS 2019. I will introduce a method for formally verifying properties of probabilistic multi-agent systems with a possibly unbounded number of agents. I will define our novel semantics, which is both parameterised (admitting an arbitrary number of agents) and stochastic. After observing that the verification problem against PLTL specifications is in general undecidable, I will introduce our partial decision procedure for the problem. This decision procedure will rely on constructing an abstract system (which captures the behaviour of a possibly unbounded number of agents) using a counter abstraction technique. I will show this technique to be sound but incomplete, and present our experimental implementation of this method, based on the probabilistic model checker PRISM. Finally, I will show the results we obtained when using our tool to analyse a foraging protocol from swarm robotics.