Why don't you try using PlusCal/TLA+ on some portion of the code at work (if you still care to stay there) to prove its effectiveness? Whittle down the code to something basic to show how it'd work so your manager/co-workers can see for themselves on code that they're reasonably familiar with.

Unless your manager/colleagues are intimately familiar with such tools, I'd think that your touting their usage at work, is more like wishful thinking.