Trains – leaderless total-order broadcast in Rust, formally verified
Trains is a Rust implementation of a leaderless total-order broadcast protocol, formally verified for correctness. It provides a decentralized approach to ordering messages without relying on a single leader, making it resilient to failures. The project aims to offer high reliability for distributed systems through formal verification techniques.
背景メモ
Trainsは、Rustで実装された「リーダーレス・トータルオーダー・ブロードキャスト」ライブラリ。分散システムにおいて、どのノードも特別なリーダーにならずに全メッセージの順序を全ノードで一致させる（トータルオーダー）手法で、TLA+による形式検証が行われている。同種の機能を提供するPaxosやRaftとは設計思想が異なり、特に信頼性が厳しく要求されるシステム（データベースのコンセンサス層など）で注目される。GitHub上で公開中。