Amazon Web Services (AWS) is a cloud computing services provider that has made significant investments in automated reasoning to check the correctness of its internal systems and to provide assurances to customers. We are using SAT and SMT solvers more than one billion times a day, both for “real-time” queries in customer security (checking security policies and verifying network protections), and also for large queries involving code and hardware reasoning that are at the limits of what can be feasibly solved by current solvers. Supporting reasoning at this scale and volume requires careful examination of the problems to be solved and a clear focus on operations to ensure our analyses are consistently trustworthy and performant. I will describe some lessons learned and ofer some directions for the community that should allow us to scale further, increase trust, and solve the next billion queries a day.