Show and tell : TRAINS: a leaderless, formally-verified total-order broadcast — \~2,400 lines of Rust, checked seven ways

announcements
1

I rebuilt a total-order broadcast protocol I helped invent in the 1990s (originally for power-plant control) from scratch in Rust, and put the core through seven independent verification methods.

The Rust-relevant parts:

  • ~2,400-line no_std-friendly, I/O-free sync core (trains-core) — which is what makes it tractable to verify.
  • Kani/CBMC bounded model-checking of the Rust itself; BTreeSet over HashSet specifically to keep Kani tractable.
  • A reference impl + differential random testing (proptest) diffing it against production code (~12k random schedules), plus crash-injection fuzzing — all runs in CI.
  • TLS ring transport on rustls (no OpenSSL).
  • Spec-level: TLA+/TLC, Apalache, an Ivy parameterised proof, runtime trace validation. The model checker caught a real ordering violation the original design had.

Write-up: https://yeychenne.hashnode.dev/trains-formally-verified
Code (MIT): GitHub - yeychenne/trains-rust: TRAINS total-order broadcast ring — formally verified Rust implementation with online node rejoin/re-admission · GitHub

Happy to go deep on the verification setup or the tricks that made bounded model-checking work.

2

Follow-up for anyone interested in the practical side: I wrote up trains-valkey, which puts an unmodified Valkey/Redis behind this ring for loss-free failover — the thing Sentinel gives up. Separate thread here: Show and tell: trains-valkey — loss-free Redis/Valkey failover via a total-order ring proxy (Rust)