[ahelwer]

Well, you can't rewrite anything in TLA+. It's a formal specification language, not verification language. So you usually use it to catch spec- or algorithm-level logic & concurrency bugs then manually write the code to correspond to your TLA+ spec. People get really hung up on this last step, but I can tell you as a professional programmer that implementing code to follow a TLA+ spec is extremely easy - all the intellectual heavy lifting has already been done! - and avoids the extremely costly effort required to fully formally verify computer code. It's a great cost/benefit ratio.