Appreciate the paper as I didn&#x27;t have that interesting work. Once again, though, they&#x27;re focused on the details of concurrent (eg protocol-like) work instead of verifying concrete, sequential programs. They claim in the paper to be able to prove absence of runtime errors but don&#x27;t give much detail. They also aim to do more on that leveraging Frama-C but again no detail. So, your example shows it a work in progress for TLA+ rather than work done several times over as in Coq or Isabelle work.<p>It does support the use of TLA+ for some aspects of C verification or specification along with integrating into the right tool (Frama-C). I&#x27;ll probably do the re-survey on TLA+ use I mentioned earlier due to this paper.