Ребята из Antithesis(я хз кто это) протестировали несколько популярных реализаций протокола Raft в своей среде детерминированной симуляции с инжекцией сбоев. Они выбрали HashiCorp Raft, Aeron Cluster, OpenRaft и MicroRaft. И да, они нашли критические баги в каждой из них, нарушающие главный инвариант - state machine safety.
На примере HashiCorp Raft подробно разбираются три бага:
- гонка асинхронных heartbeat'ов с основным потоком, нарушающая консенсус и безопасность выборов;
- deadlock при передаче лидерства, навечно блокирующий кластер;
- и livelock при установке снапшотов из-за несоблюдения правила из спецификации.
Они приходят к выводу, что формальная верификация сама по себе не гарантирует корректности, поскольку между спецификацией на TLA+ и продакшен-кодом остаются неявные допущения.
И еще забавно, что хватило простой нагрузки вроде "цепочки блоков" в сочетании с симуляцией сбоев, чтобы эти проблемы вскрылись
