It&#x27;s typicaly not tractable to prove that a system is safe.  For example, RethinkDB used the raft consensus algorithm, which on its own is proven correct, but due to a bug could in some cases break linearization.  Jepsen was able to uncover this.<p>The best method we currently have for demonstrating that large systems are safe is to try really hard to prove that they are unsafe and fail.