主要观点：在亚马逊云服务（AWS）应用自动化推理的十年中，发现形式验证代码往往比未验证代码性能更高，原因是验证过程中的错误修复能积极影响代码运行时，还能让开发者更有信心探索优化，形式验证代码更易更新修改操作。文中分享了与 DARPA 讨论的三个例子，包括 S3 索引子系统通过形式验证找到并修复 bug 提高更新频率、IAM 服务通过形式验证实现可证明安全并优化代码、在 AWS Graviton 上利用自动化推理优化加密算法部署速度等。自动化推理形成了一个良性循环，提高了 AWS 云服务的安全性、可靠性和性能，AWS 是首家大规模应用自动化推理的云提供商，未来有望实现大规模云架构关键属性的自动证明。
关键信息：

• [Defense Advanced Research Projects Agency (DARPA)]：美国国防高级研究计划局
• [Amazon Web Services (AWS)]：亚马逊云服务
• [Amazon Simple Storage Service (Amazon S3)]：亚马逊简单存储服务
• [AWS Identity and Access Management (IAM)]：AWS 身份和访问管理服务
• [AWS Graviton]：AWS Graviton 处理器
• [ARM instruction set]：ARM 指令集
  重要细节：
• S3 索引子系统是 S3 的关键组件，包含大型复杂数据结构和优化算法，曾有 bug 难以确定原因，通过形式验证找到并证明无同类 bug，提高更新频率至每 1 - 2 个月。
• IAM 服务每秒处理超 12 亿请求，是 AWS 中最安全关键和高规模的软件，通过形式验证实现可证明安全，构建新的更高效实现并优化代码，性能提升 50%。
• 在 AWS Graviton 上利用自动化推理优化加密算法，如 RSA 和椭圆曲线加密，提高性能和部署速度。
• AWS 是首家大规模应用自动化推理的云提供商，随着工具采用增加，投资可改善工具可用性和可扩展性，提高云服务安全性和性能，最终为客户节省成本。