Formal Methods in Industry: A Critical Evaluation of Their Use at Amazon Web Services

Formal methods have long promised enhanced software reliability through rigorous mathematical reasoning, yet concerns over scalability, cost, and accessibility have historically limited their industrial adoption. This paper critically evaluates the public record on the use of formal methods in engineering at Amazon Web Services (AWS). Drawing on publicly available case studies, engineering reports, and technical documentation, we examine reported applications of model checking, SMT solving, and lightweight formal methods across domains such as distributed systems, cloud networking, cryptography, and security policy verification. We organise the analysis around 16 targeted questions across five themes: (1) technical impact, (2) organisational adoption, (3) scalability in complex and heterogeneous systems, (4) long-term strategic value, and (5) future directions. By placing these AWS case studies alongside historical precedents at companies such as IBM, Microsoft, and Google, we highlight both continuity and innovation in industrial practice. Across the published case studies, authors report benefits such as early bug detection, performance optimisation, and strengthened security assurance, including integration with CI/CD workflows in some settings. However, the evidence base is selective and does not support organisation-wide claims about prevalence, cost-effectiveness, or ROI; quantitative baselines are sparse, and survivorship bias is plausible. We discuss the resulting methodological limits, highlight challenges such as maintaining specifications under continuous evolution, and outline a research agenda to improve empirical validation, methodological refinement, and the preservation of industrial verification artefacts.