主要观点：云数据库面临节点故障下的可用性和耐久性挑战，现代云数据库通过分离计算和存储来解决，分布式日志服务是其核心。多数系统使用共识协议如 Paxos 管理日志复制，但有开销大等问题，Taurus 系统提出用三个节点写数据的简单替代方案，虽有吸引力但引入复杂故障场景，需用形式验证确保正确性。
关键信息：

• 云数据库需解决节点故障下的可用性和耐久性问题，现代方法是分离计算和存储，通过复制预写日志保证耐久性。
• 多数系统使用 Paxos 等共识协议管理日志复制，有高写放大和多网络往返开销。
• Taurus 系统用三个节点写数据，系统架构简单，有多种优点，如只需三个节点实现三副本等。
• 简单设计引入复杂故障场景，传统测试难以发现，需用形式验证确保正确性。
• 将构建并验证受 Taurus 启发的完整日志系统，分步骤用 P 语言建模和验证，后续会有系列文章。
  重要细节：
• 现代云数据库将数据库引擎设为无状态，预写日志在多个节点复制。
• Taurus 系统写数据时若写失败就选三个不同节点继续，协调通过外部共识实现。
• 形式验证用 P 语言可系统探索系统状态和转换，捕捉传统测试遗漏的细微错误。
• 系列文章包括多个部分，分别建模不同情况并逐步完善验证系统，完整代码在 github 上。