Trains – Rust实现的无领导全序广播，经过形式化验证

- 该项目用 Rust 实现了一种"无领导全序广播"协议，并通过形式化验证保证正确性。全序广播是分布式系统的核心原语：它确保所有节点以相同顺序收到相同消息，是构建共识机制（如 Paxos、Raft）的基础。 - "无领导"意味着集群中不存在固定的主节点，所有节点对等协作，消除了单点故障和主节点选举的开销。 - 项目使用 TLA+ 和 Verus 等形式化验证工具对协议进行数学级正确性证明，而不仅仅是测试。这对可靠性要求极高的系统（如区块链、分布式数据库）意义重大。 - Rust 语言的选择带来了内存安全和零成本抽象，适合系统级基础设施开发。 - 该项目面向专业分布式系统开发者，目前处于早期阶段，不是面向最终用户的产品。