Modern software systems are exposed to various types of uncertainties, such as dynamics in the available resources that are difficult to predict and goals that may change during operation. Self-adaptation equips a software system with a feedback loop that collects additional knowledge at runtime, monitors the system and adapts it when necessary to maintain its quality goals, regardless of uncertainties. One challenging problem of self-adaptation is to provide guarantees for the goals that are subject of adaptation. In this paper, we present the ActivFORMS runtime environment to realise self-adaptation with guarantees. With ActivFORMS designers model and verify a feedback loop. The verified models can directly be deployed on top of a virtual machine that executes the models to realise adaption. The approach avoids coding of the models, which is an error-prone task. The runtime environment visualises the executing models, the state of the goals, and it supports on the fly updates of the models and goals. We illustrate the approach with an adaptation scenario of an IoT building security example.