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

Дата публикации: 01-07-2026 09:54:50

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.
3 posts - 1 participant
Read full topic

Схожие новости

#	Наименование новости	Тональность	Информативность	Дата публикации
1	Looking for contributors: Rust transparent proxy & protocol parsing project	5	7	08-07-2026
2	Maplike - Crate with traits for abstract containers and operations on them	2	7	06-07-2026
3	Mqtt-typed-client 0.2: a type-safe async MQTT client on top of rumqttc	5	7	08-07-2026
4	Chainything : A DAG-based pipeline execution engine & visual UI (with AI generation)	2	7	29-06-2026
5	Test That! 0.5: A powerful test assertion library for Rust	5	7	28-06-2026
6	BloomCraft: twelve Bloom filter variants under one API, looking for feedback	5	6	06-07-2026
7	[Project Announcement] tinyxml2-rs: A high-performance, drop-in Rust implementation of TinyXML2	5	7	01-07-2026
8	CPUX - retained-mode GUI framework	0	5	01-07-2026
9	LiberSystem - the new OS written in Rust	0	5	07-07-2026
10	Покрываем REST-сервис на Rust тестами	0	5	05-05-2026

Классификация: Пресс-релизы. Схожих патентов: 0. Схожих новостей: 10. Тональность: 7. Информативность: 8. Источник: users.rust-lang.org.