This is fascinating. The AWS Auth system handles over a billion requests a second - how do you make it run faster, safely make changes and test at scale? With formal proofs.
https://www.amazon.science/publications/formally-verified-cloud-scale-authorization
Formally verified cloud-scale authorization
All critical systems must evolve to meet the needs of a growing and diversifying user base. But supporting that evolution is challenging at increasing scale: Maintainers must find a way to ensure that each change does only what is intended, and will not inadvertently change behavior for existing…