<div dir="ltr"><div>I am trying to use TLA from Agda. I have just managed to prove the TwoPhase refinement of TCommit. I have some thoughts and questions about this that relates to Agda too. <br></div><div dir="ltr"><a href="https://groups.google.com/d/msg/tlaplus/d_Mm7lYMQaI/2XdKAQpIDgAJ" target="_blank">https://groups.google.com/d/msg/tlaplus/d_Mm7lYMQaI/2XdKAQpIDgAJ</a></div><div dir="ltr"><br></div><div>The main problem is that specifications have global invariants that need to be proven, to prove that they are a refinement of another. But then, we lose the ability to use the restrictions of the refinement as a guide for the definition of the refining spec.</div><div><br></div><div>In other words, I want to postpone the definition of the refining spec as much as possible and introduce restrictions as soon as possible, in order to have type-driven development.</div><div>This is not very easy with global invariants.</div></div>