在 Raft 实现中寻找 Bug
来源：antithesis.com — 2026-07-27
📋 概述
Antithesis 团队对他们测试过的每一个 Raft 实现都发现了 Bug——包括 HashiCorp Raft、Aeron Cluster、OpenRaft 和 MicroRaft，尽管这些项目投入了形式化方法、代码审查、单元测试和多年生产环境验证。发现的 Bug 表现为违反 Raft 的核心不变式——状态机安全性（全序交付）。文章详细拆解了测试中暴露的四个关键假设，揭示了规范到代码之间存在巨大的实现鸿沟。
🔑 核心要点
- 测试过的所有 Raft 实现都有 Bug，包括 HashiCorp Raft 等成熟项目。
- Bug 表现为违反 状态机安全性（全序交付），这是 Raft 最核心的不变式。
- 尽管有形式化 TLA+ 规范、详细实现指南、代码审查和生产验证，Bug 依然存在。
- 规范与代码之间的假设鸿沟是根本原因：同步进程、请求-响应映射、任期一致性等假设在实践中常被打破。
💡 金句
尽管投入了形式化方法、细致的代码审查、单元测试和多年的生产环境测试，我们测试的每一个 Raft 实现中都有 Bug。
👍 0
👎 0
← 返回 Lobsters 首页