This thesis investigates the use of formal methods to verify cloud system designs against Service Level Agreements (SLAs), towards providing guarantees under uncertainty. We used WATERS (the Waikato Analysis Toolkit for Events in Reactive Systems), which is a model-checking tool based on discrete event systems. We created models for one aspect of cloud computing, horizontal autoscaling, and used this to verify cloud system designs against an SLA that specifies the maximum request response time. To evaluate the accuracy of the WATERS models, the cloud system designs are simulated on a private Kubernetes cluster, using JMeter to drive the workload. The results from Kubernetes are compared to the verification results from WATERS. A key research goal was to have these match as closely as possible, and to explain the discrepancies between the two. This process is followed for two applications: a default installation of NGINX, a web server with a fast but variable response time, and a hand-written Node.js program enforcing a fixed response time. The results suggest that WATERS can be used to predict potential SLA violations. Lessons learned include that the state space must be constrained to avoid excessive checking times, and we provide a method for doing so. An advantage of our model checking-based technique is that it verifies against all possible patterns of arriving requests (up to a given maximum), which would be impractical to test with a load testing tool such as JMeter. A key difference from existing work is our use non-probabilistic finite state machines, as opposed to probabilistic models which are prevalent in existing research. In addition, we have attempted to model the detail of the autoscaling process (a “white-box” approach), whereas much existing research attempts to find patterns between autoscaling parameters and SLA violation, effectively viewing autoscaling as a black-box process. Future work includes refining the WATERS models to more closely match Kubernetes, and modelling other SLO types. Other methods may also be used to limit the compilation and verification time for the models. This includes attempting different algorithms and perhaps editing the models to reduce the state space.