A health rule that retired healthy hardware

The simulation said a shrinking quorum does a third more work than fixed triple redundancy. The next step was a program that does it for real: three replica processes computing the same hash, a voter, and faults injected on a schedule. The first version was 407 lines of C++.

Its health rule retired a replica that was outvoted three times within 200 ticks. That reads like caution and was the opposite. Random upsets land on any replica, so three in one window could retire a healthy one, and the shrinking quorum ended up with less hardware than the triple redundancy it was meant to beat.

The rewrite in Rust, 21 minutes later, treats three strikes as a reason to ask, not to act. The replica runs a known-answer test, a fixed input whose result is known. Passing means the upsets were transient, and its strikes are cleared. Failing retires it. A scenario script now checks over ten seeds that the shrinking quorum never delivers fewer correct results than fixed triple redundancy, and Kani proves the two policies make the same decision while two or more replicas live.

With one replica stuck and another dead, fixed triple redundancy delivered 8,993 correct results and rejected 11,007. The shrinking quorum delivered 14,490 and rejected 10.

The cost stays in the README, in a section of its own. On the last replica, a stuck fault is only caught by the periodic test, every 64 ticks. With two replicas lost and the third stuck, that came to 24 wrong results before the system stopped. Fixed triple redundancy would have stopped sooner and delivered none.