Neither the specification nor the analysis contain a formal, verifiable specification. How can one test an invariant and properties and make real conclusions about the safety&#x2F;liveness of Redlock without it?<p>Is it not useful to do so?