I reimplemented a CAP-aware total-order broadcast protocol in Rust and verified it seven ways

In the early 1990s, in a research lab at Cegelec near Paris, a small team I was part of built a way to keep industrial control systems running through hardware failures — the kind that supervise power