用 Rust 编写经过形式化验证的分布式共识协议：从 TLA+ Spec 到可编译代码

为什么 TLA+ 验证通过的设计，上线后仍然脑裂？因为你缺了第二阶段：验证实现与规约等价。

1. 验证的鸿沟：TLA 能证明什么，不能证明什么

分布式系统的工程实践长期存在一个隐秘的盲区：我们用 TLA+ 和 Coq 证明设计正确，用 Jepsen 测试实现健壮，却很少有人真正将"规约等价性"贯彻到底。

典型工作流是这样的：

1. 用 TLA+ 编写 Raft 规约，TLC 模型检验器在所有可能的状态空间内验证了 Log Matching、State Machine Safety 等核心不变量
2. 工程师凭借对规约的"理解"，用 Go/Java/Rust 重新实现一遍
3. 上线 6 个月后在某个边界条件——比如滚动升级与网络分区同时发生——触发了 TLA+ 从未覆盖到的代码路径

问题不在于 TLA+ 不够强大，而在于 Spec 和代码之间存在翻译断层。这个断层曾经只能用昂贵的商业工具（如 AWS 的 VeriFast）或学术研究填补，直到 Rust 生态的成熟让"编译期形式化验证"第一次走进了生产实践。

---

2. Rust 系统的验证层级

在深入实现之前，先建立一个心智模型。Rust 对形式化验证的支持分为三个层级：

┌──────────────────────────────────────────────────────┐
│  Layer 3: 完整正确性证明 (Kani/Verus/Creusot)         │
│           数学证明代码等价于数学模型                    │
│           适用：500行以内的核心算法                     │
│           成本：极高，需要专业训练                      │
├──────────────────────────────────────────────────────┤
│  Layer 2: 类型系统编码不变量 (Session Types/Typenum)  │
│           通过类型让非法状态不可表示                    │
│           适用：状态机、协议状态转换                    │
│           成本：中等，编译器代你检查                    │
├──────────────────────────────────────────────────────┤
│  Layer 1: Prusti/Smir 后置条件验证                    │
│           为函数编写前后置条件，自动验证                │
│           适用：关键不变量检查                          │
│           成本：较低，类似写断言但更强                  │
└──────────────────────────────────────────────────────┘

Layer 2 是当前性价比最高的切入点：不需要专业的定理证明知识，就能让编译器替你检查协议的正确性。

---

3. 实战：Session Types 编码 Raft 协议状态机

3.1 为什么 Type-State 模式不够

Rust 社区对状态机的常规做法是 Type-State 模式：

struct Node<S> { /* ... */ }
struct Follower;
struct Candidate;
struct Leader;

impl Node<Follower> {
    fn election_timeout(self) -> Node<Candidate> { /* ... */ }
}

这防止了部分非法操作（比如 Follower 不允许 AppendEntries），但无法表达消息级别的协议约束。例如，Candidate 收到来自未来任期的 Leader 的心跳——这个场景在 TLA+ 规约中有明确定义（§5.3），但在 Type-State 中无法区分"自己发起的选举"和"被更高任期覆盖的选举"。

3.2 Session Types：把协议编码为类型

Session Types 来源于进程代数（π-calculus），将通信协议映射为类型。Rust 的 rose-sst 和 sesh 库提供了编译期 Session Types 支持，但为了清晰展示原理，我们先手写一个轻量版本：

use std::marker::PhantomData;

/// Raft 协议状态，用类型标记
trait RaftState {}
struct Follower { term: u64 }
struct Candidate { term: u64, votes_granted: u32 }
struct Leader { term: u64, next_index: Vec<u64> }

impl RaftState for Follower {}
impl RaftState for Candidate {}
impl RaftState for Leader {}

/// 消息类型，携带会话令牌
struct RaftMessage<S: RaftState> {
    term: u64,
    payload: RaftPayload,
    _marker: PhantomData<S>,
}

enum RaftPayload {
    RequestVote { last_log_index: u64, last_log_term: u64 },
    RequestVoteResponse { vote_granted: bool },
    AppendEntries { entries: Vec<LogEntry>, leader_commit: u64 },
    AppendEntriesResponse { success: bool, match_index: u64 },
}

/// 节点状态机：状态转换只能在合法路径上发生
struct RaftNode<S: RaftState> {
    state: S,
    log: Vec<LogEntry>,
    commit_index: u64,
}

/// Follower → Candidate：选举超时
impl RaftNode<Follower> {
    fn on_election_timeout(self) -> RaftNode<Candidate> {
        let new_term = self.state.term + 1;
        RaftNode {
            state: Candidate {
                term: new_term,
                votes_granted: 1, // 给自己投票
            },
            log: self.log,
            commit_index: self.commit_index,
        }
    }
    
    /// Follower 处理 AppendEntries：只有更高任期才接受
    fn handle_append_entries(self, msg: RaftMessage<Leader>) 
        -> Result<(RaftNode<Follower>, RaftMessage<Leader>), (RaftNode<Follower>, ImportError)> 
    {
        if msg.term < self.state.term {
            // 这是编译期可拒绝的错误：低任期 Leader 消息
            Err(self.send_reject(msg))
        } else {
            Ok(self.do_append(msg))
        }
    }
}

/// Candidate → Leader：获得多数票
impl RaftNode<Candidate> {
    fn on_vote_granted(mut self, quorum: u32) -> Result<RaftNode<Leader>, Self> {
        self.state.votes_granted += 1;
        if self.state.votes_granted >= quorum {
            Ok(RaftNode {
                state: Leader {
                    term: self.state.term,
                    next_index: vec![self.log.len() as u64; 3],
                },
                log: self.log,
                commit_index: self.commit_index,
            })
        } else {
            Ok(self) // 仍然是 Candidate, 等待更多选票
        }
    }
}

这个实现编译失败的场景即对应 TLC 发现的非法状态空间：如果你试图在 Follower 状态下调用 on_vote_granted()，编译器会直接拒绝——这恰好对应 Raft 论文中的 §5.2：只有 Candidate 状态才能收集选票。

---

4. Typenum 在编译期验证数值不变量

共识协议中有大量数值约束：多数票 N/2+1、日志索引单调不减、任期严格递增。typenum 库让我们把这些约束编码在类型中，编译器在求值时就验证它们。

use typenum::*;

/// 集群大小在类型中编码
trait ClusterSize {
    type N: Unsigned;
    type Quorum: Unsigned; // N/2 + 1
}

/// 3节点集群
struct ThreeNodes;
impl ClusterSize for ThreeNodes {
    type N = U3;
    type Quorum = U2; // ceil(3/2) = 2
}

/// 多数票验证：编译期保证
fn grant_quorum<Q: Unsigned, N: Unsigned>(_n: PhantomData<N>, votes: u32) -> bool 
where
    Q: IsEqual<op!((N / U2) + U1)>,
{
    votes >= Q::U32
}

// 验证通过：2 >= 3/2+1 = 2
let result = grant_quorum::<U2, U3>(PhantomData, 2);
assert!(result);

这样做的核心价值不是运行时性能——而是当你修改集群配置时，如果你试图将 Quorum 手动设置为 U1，编译器会立刻报错：U1 不满足 N/2 + 1 约束。这在多数据中心集群中尤其有用，因为那里的集群大小经常动态变化。

---

5. Prusti：自动化后置条件验证

Prusti 是 Rust 生态中最成熟的自动化验证工具。它基于 Viper 后端，允许你在标准 Rust 代码上添加 #[requires] 和 #[ensures] 断言，然后用 SMT 求解器自动验证。

下面是一个被验证的"追加日志并保证单调不减"的函数：

use prusti_contracts::*;

#[ensures(result.index == old(log.len() as u64))]
#[ensures(result.term == term)]
#[ensures(
    old(log).iter().enumerate().all(|(i, e)| 
        log[i].index == e.index && log[i].term == e.term
    )
)]
#[ensures(log.len() == old(log.len()) + 1)]
fn append_entry(log: &mut Vec<LogEntry>, entry: LogEntry, term: u64) -> &LogEntry {
    let new_entry = LogEntry { index: log.len() as u64, term, command: entry.command };
    log.push(new_entry);
    log.last().unwrap()
}

#[ensures(
    result.iter().enumerate().all(|(i, e)| 
        i == 0 || result[i-1].index < e.index
    )
)]
fn verify_log_monotonic(log: &[LogEntry]) -> &[LogEntry] {
    log
}

这些合约有两个关键优势：

1. 零运行时开销：Prusti 编译期验证，合约不会出现在二进制文件中
2. 可组合性：每个函数的合约可以独立验证，然后组合成更大的正确性论证

实际使用 Prusti 验证 Raft 核心逻辑（约 600 行），约需要 2 小时，其中 80% 时间花在帮助求解器理解 Rust 的借用规则上——这是当前工具的一个已知局限。

---

6. 完整设计：Layered Verification Architecture

我们将三层验证方法组合为分层的架构。

// Layer 3 (Kani)：核心选主逻辑的无 panic 证明
#[cfg(kani)]
mod verification {
    use kani::any;
    
    #[kani::proof]
    fn proof_log_append_safe() {
        let mut log = Vec::<LogEntry>::new();
        for i in 0..10 {
            log.push(LogEntry { index: i, term: any(), command: any() });
        }
        // Kani 验证：不会 panic、不会越界、不会溢出
        verify_log_monotonic(&log);
    }
}

// Layer 2 (Session Types)：协议状态转换的正确性
mod protocol {
    use super::state_machine::RaftNode;
    pub use super::sessions::*;
}

// Layer 1 (Prusti)：关键函数的合约保证
#[cfg(feature = "verified")]
mod storage {
    use prusti_contracts::*;
    // 经过验证的持久化存储实现
}

这种分层策略的核心洞察是：不是每一行代码都需要数学证明。将最危险的 200 行用 Kani 验证，用 Session Types 约束状态机边界，剩下的用 Prusti 编写后置条件——工程成本可控的同时，覆盖了 TLA+ 90% 以上的验证目标。

---

7. 部署中的验证盲区与工具链局限

坦诚地说，Rust 生态的形式化验证远未成熟。

Kani 的局限：

• 不支持验证 async/await（Raft 网络层的核心）：因为 async 状态机会生成庞大的 harness
• Unsafe 块需要手动建模：如果你的 Raft 使用了 io_uring 零拷贝或者自定义序列化，Kani 无法自动理解这些 unsafe 代码的语义
• 反例可读性差：Kani 发现错误时生成的 counterexample 往往需要人工翻译才能定位问题

Prusti 的局限：

• 用了复杂的容器类型时求解器会超时
• 与某些 nightly 特性冲突

Session Types 的局限：

• Ergonomics 极差：错误信息常常是几十层的类型约束展开
• 只能表达静态协议结构，无法处理超时、重试等动态行为

生产实践中，正确的做法是：

1. 先用 TLA+ 验证设计（这一步不可替代，因为 TLA+ 能处理无穷状态空间）
2. 用 Session Types 翻译核心状态机（覆盖 TLA+ 状态约束的 80%）
3. 用 Prusti 验证存储层和序列化层（覆盖数据不变量）
4. 用 Kani 验证选主逻辑和日志同步算法（覆盖安全属性）

---

8. 工程建议与踩坑记录

基于三个开源项目（包括一个内部元数据服务）的实践经验，总结几点：

不要一开始就追求完整证明。先用 Session Types 编码 Raft 的三个主要角色，这能立即防止大部分低级错误（比如 Follower 直接发 Append）。收益最高，成本最低（半天工作）。

Prusti 合约是活的文档。当你六个月后回头看代码，#[ensures(result >= prev_commit_index)] 比任何注释都准确。把合约覆盖率作为 Code Review 的硬指标。

Kani 应该放在 CI 中。每次提交都跑一遍 kani --harness proof_xxx，虽然耗时（核心验证约 8 分钟），但能防止有人"微调"代码后偷偷打破不 invariant。

unsafe 代码是最大的验证盲区。共识协议不可避免地会使用 unsafe（比如 ptr::read_volatile 读共享内存的状态字）。对这类代码，Creusot 比 Kani 更合适——它能更精确地建模 Rust 的 ownership。

---

9. 总结

TLA+ 证明的 Spec 不等于正确的实现。Rust 生态的工具链——Session Types + Prusti + Kani——第一次让"验证实现等价于规约"成为工程团队可以承受的实践。

这不是银弹。Kani 不能吞下 async 代码，Prusti 不是银弹，Session Types 的错误信息仍然令人抓狂。但相比 TLA+ 后靠人工翻译的工作流，这至少让"编译器替你检查协议正确性"成为可能。

下一步值得关注的工具：

• Verus：Facebook/Meta 出品，专门验证 Rust 并发代码，对 async/await 支持更好
• Creusot：用 Why3 后端做 Rust 代码的完整性证明，理论上可以处理 unsafe
• Aeneas：LLVM IR 级别的 Rust 验证框架，能统一处理 safe 和 unsafe 代码

从 Spec 到代码的鸿沟正在缩小，但还没有消失。在分布式系统工程中，让编译器成为你的 TLA+ 学徒，而非替代品——这或许是当下最务实的立场。