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.

1 post - 1 participant

Read full topic