So since it depends on the correctness of the underlying system is there a TLA+ (or other) proof for that? Last time jepsen ran on redis it showed that it was b

So since it depends on the correctness of the underlying system is there a TLA+ (or other) proof for that? Last time jepsen ran on redis it showed that it was broken unless something has changed in the meantime.