It's almost certainly not worth the effort, given what you said about your work domain. From what I've seen, TLA is finding a niche for modeling complex concur

It's almost certainly not worth the effort, given what you said about your work domain. From what I've seen, TLA is finding a niche for modeling complex concurrent/distributed algorithms. I'd recommend design by contract as a lighter way of verification. And if you don't like the TLA syntax, you could try a verification tool similar to TLA called SPIN, since it kind of looks like C. The reference for SPIN is the book written by the tool's author.