1. Writing formal proofs in TLA+ (or in any other proof assistant) is almost always a waste of time. If the proof is very easy, you can certainly do it, but the

1. Writing formal proofs in TLA+ (or in any other proof assistant) is almost always a waste of time. If the proof is very easy, you can certainly do it, but then you don't need to unless it's a strict requirement or an academic project whose entire purpose is to show that a formal proof is possible rather than some functional correctness requirement. And if the proof is not easy, then there are better methods, like using TLA+'s model checker. 2. Putting references to the TLA+ spec in the code could be nice and useful. 3. You should realize that the benefit from a powerful tool like TLA+ comes when it helps you reason about things that are hard for you to do, and those are hardly ever at the code level. So while using a code-level tool like Why3 to prove some routine is cool, it is hardly ever done in practice, because that's hardly every where the problems you need help with are. Those are usually found in complex interactions between machines, or your program and the user etc.. So often TLA+ is most useful when the specification is so far above the code level that a direct link is not entirely useful. Having said that, you could use TLA+ to actually prove at the code level by compiling your code to TLA+, as has been done with Isabelle or Coq. This has been done for TLA+ with C and Java, but in practice, code-level verification is not where you'll get the most bang for your buck.