Formal methods have been successfully applied in domains such as microprocessor hardware design and aerospace. However, despite 50 years of research and development, we have not seen wide adoption of formal methods for large and complex systems such as web services, industrial automation, or enterprise support software. One of the key difficulties when proving security, safety, and robustness of these systems is the problem of finding the models of system architectures necessary for analysis. Additionally, the size of the potential user community and the business value typically does not justify the creation of scalable and easy-to-use tools for formal verification. With the cloud, much of this has changed. Descriptions of cloud services provide accurate models in the form of computer-readable contracts. These contracts establish and govern how the system behaves and in many cases these models are amenable to formal analysis at scale. Most importantly, since those models are used by a large user community, it is now economically feasible to build the tools needed to verify those models. In this talk, we discuss the trend of constructing practical and scalable cloud-based formal methods at Amazon Web Services and how they can easily be used by customers – sometimes with just one-click.