Реализация Raft на TypeScript под сидированной симуляцией: каждый тик, каждая задержка сообщения и каждое падение узла берутся из сида. На двадцать пятом прогоне две реплики применили разные значения — при том, что правила алгоритма выполнялись все до одного.

Интересен не сам баг, а то, какая проверка его поймала. И вопрос, который из этого следует: откуда я знаю, что остальные проверки вообще на что-то смотрят.

Проверка модели полным перебором упирается в комбинаторный взрыв, и практически вся инженерия в этой области — не про сам поиск, а про то, как его избежать. Две классические техники — редукция по симметрии и редукция частичных порядков — описаны в литературе десятилетиями, но их эффект обычно приводится либо асимптотически, либо на одном показательном примере.

Ниже — измерение на работающей реализации: во сколько раз каждая редукция сокращает пространство состояний, сколько она стоит в пересчёте на состояние, на каких спецификациях она не даёт ничего, и — главное — экспериментальная проверка того, что четыре условия ample‑множества действительно необходимы, а не унаследованы из статьи без разбора.

Три результата, ради которых стоит читать дальше:

Набор тестов, который всегда зелёный, содержит непроверяемое допущение: он может ловить ошибки, а может не смотреть вообще — по цвету это неразличимо.

Я писал реализацию Raft на TypeScript и построил вокруг неё музей багов: семь экспонатов, каждый выключает ровно одно правило алгоритма и требует, чтобы харнесс поймал это — с сидом и с именем нарушенного свойства.

Один экспонат появился не по плану. Харнесс нашёл баг в самой реализации: все пять свойств безопасности держались, логи совпадали, никто не падал — и на двадцать пятом сиде две реплики разъехались навсегда. Разбираю, почему так вышло, как устроен харнесс и чего этот метод не доказывает.