主要观点：Amazon Web Services (AWS)致力于提供可完全信任的可靠服务，以系统正确性为基石维持高安全等标准，通过多种形式方法确保服务正确性及性能提升。
关键信息：

• 采用 TLA+确保关键服务正确性，能早期识别并消除传统测试难以发现的细微错误，实现性能优化同时保持系统正确性。
• 开发 P 编程语言，以其建模分布式系统的优势，用于 S3 等服务的一致性迁移及系统设计验证。
• 运用轻量级形式方法，如属性测试、确定性模拟、持续模糊测试等，加速开发并提升系统测试覆盖度。
• 推出 Fault Injection Service 使客户能进行故障注入测试，缩小正常情况与错误情况的测试差距。
• 关注系统的亚稳性和突发行为，借助离散事件模拟等理解系统 emergent 行为。
• 对于关键安全边界进行形式证明，如 Cedar 授权政策语言和 Firecracker 虚拟机监视器的证明。
• 形式方法不仅确保正确性，还能提升系统性能，如在 Aurora 数据库中的应用。
  重要细节：
• 15 年前 AWS 软件测试主要依赖构建时单元测试和有限的部署时集成测试，如今已进化为整合多种形式方法。
• PObserve 工具用于验证分布式系统在测试和生产中的正确性， bridging 系统设计规范与生产实现。
• 在 Amazon S3 的 ShardStore 中，属性测试结合多种技术加速开发并测试正确性。
• 确定性模拟测试将系统属性测试移至构建时，加速开发并提升行为覆盖度。
• Fault Injection Service 被 AWS 客户和内部广泛使用，用于验证架构的弹性机制。
• 亚稳性行为在云系统中常见，传统形式方法难以涵盖，需借助离散事件模拟等。
• 在 Cedar 授权政策语言和 Firecracker 虚拟机监视器中，通过形式证明确保关键安全边界的正确性。
• 形式方法在高、低级别代码优化中都有成效，如在 AWS 的 RSA 加密方案优化中。
• 形式方法面临学习曲线陡峭、工具界面不友好等挑战，但未来大语言模型和 AI 助手有望改善。