（全球 TMT2024 年 11 月 13 日讯）亚马逊云科技是唯一一家大规模使用自动推理的云提供商。随着越来越多的人使用自动推理工具，亚马逊云科技在提升其可用性和可扩展性上投入更多。自动推理工具越易于使用，其功能就越强大，采用率也更高。通过证明云基础设施的正确性，亚马逊云科技的服务对看重安全的客户更具吸引力，不仅提高了安全性，还能更快地为客户提供高性能代码，并节省成本。

在应用自动推理超过 10 年中，亚马逊云科技发现经过验证的代码通常比未经验证的代码性能更好，因为验证过程中的 bug 修复提升了运行性能。自动推理让开发人员有信心探索额外优化，提高系统性能，并减少日志分析和调试环节。在复杂分布式系统中，传统测试方法难以彻底验证所有可能状态，而自动推理通过逻辑证明快速、高效地实现相同效果。

Amazon S3 工程师每天使用自动推理防止 bug，这一技术帮助亚马逊云科技找到并解决 S3 索引子系统中的问题，使得每一两个月发布更新成为可能。同样，在 IAM 服务中，通过构建正式规范并进行数学证明，亚马逊云科技部署了新的授权引擎，实现 50% 的速度提升。这些例子表明，亚马逊云科技内部广泛应用自动推理技术，不仅用于验证正确性，还增强了安全性、可靠性及设计缺陷最小化。