Trains – leaderless total-order broadcast in Rust, formally verified

- Total-order broadcast (also called atomic broadcast) is a fundamental building block in distributed systems: it ensures all nodes in a network receive the same messages in the same order, which is essential for reaching consensus without a central coordinator. - "Leaderless" means the protocol does not rely on a single designated node (leader) to decide the message order — this avoids the single point of failure and performance bottleneck typical of leader-based systems like Raft or Paxos. - Formally verified indicates the project uses mathematical proof tools (likely TLA+ or Coq) to prove the protocol's correctness guarantees, which is rare for a Rust implementation and adds strong reliability guarantees. - Rust is a systems programming language known for memory safety and performance; implementing consensus protocols in Rust is increasingly common for production infrastructure (e.g., blockchain nodes, distributed databases).