Actually, TLA+ (again the way I understand it), after nearly 20 years of MDSE, convinced me that I would very rarely need to generate code. It's a much better value proposition to write correctly factored code. TLA+ is one of the most amazing element of Computer Science. Everyone who writes code should have at least a basic understanding of it.