It'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.

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.