Команда инфраструктуры ВКонтакте разрабатывает распределенные системы, цена ошибки в которых очень велика, потому что это фундамент для бесперебойной работы всего vk.com. В докладе поделюсь опытом, который мы наработали в ходе верификации наших систем. Расскажу, как проверяем, что система будет отвечать заданным требованиям даже в случае различных повреждений в кластере — от сети до дисков.

Пройдемся по всем этапам от зарождения идеи до ее реализации и разберём, как на каждом из них понять, что корректность не нарушена. Поговорим про TLA/TLC+, fuzzing и причинах, почему нам пришлось написать "свой" Jepsen.