This is super interesting - especially the tool they used. It looks like it interposes itself at the RPC level, unlike Jepsen which intervenes at the network level. That lets it create reproducible test cases in a distributed system, which it then minimizes so that they can be understood more easily. Very cool.