Abstract. Auto-scaling, a key property of cloud computing, allows application owners to acquire and release resources on demand. However, the shared environment, along with the exponentially large configuration space of available parameters, makes the configuration of auto-scaling policies a challenging task, for its hardness to quantify their impact on Quality of Service (QoS) provision a priori. To address this problem, we contribute to a novel probabilistic modelling and verification scheme for probabilistically verifying performance guarantees on particular rule-based auto-scaling policies. We demonstrate the usefulness, and efficiency of our model through an elaborate validation process on the Amazon EC2 cloud, by considering two types of load patterns. To the best of our knowledge this is the first work, where a formal verification scheme takes a vertical in-depth approach with respect to auto-scaling policies, by taking the cloud application provider perspective, and validated against VMs rented on a major public cloud provider, such as Amazon EC2. Our experimental results, show that it can be proven very effective in helping the cloud application owner configure an auto-scaling policy, in order to minimise the QoS violations.