Uncertainties occur in different forms: data may be noisy, mechanisms may be inherently randomised, the visibility (of e.g. a robot) may not be optimal, and the environment in which a system needs to operate may behave in an unknown manner. The central question that we will address is “Can we guarantee that AI systems are safe and resilient in the presence of such uncertainty?” We advocate using model-based, formal verification and synthesis with a particular focus on automation. We will present techniques to (a) verify uncertainty aspects modeled as randomness and to (b) use formal synthesis to complete partial designs. Several example AI models—Bayesian networks, partially observable Markov decision processes, and probabilistic programs – will illustrate the capabilities of these approaches.