I agree, and part of the issue is that if the formal methods work as intended, then by design nothing interesting happens, making their success less visible to managers that aren't paying close attention. Ideally something like TLA+ would catch a bug that you wouldn't notice for multiple years (e.g. infinite money glitches), but that means that value becomes less obvious because it can take multiple years to manifest, and that means you're waiting multiple years for TLA+ to show its value, which would be "nothing happened", which can be harder to measure.
I've debated trying to write a PlusCal->Java transpiler [1], and I haven't really ruled that out yet; while I don't think it should be necessary to have that for PlusCal to be useful, I think it would potentially sweeten the sales pitch.
[1] I think PlusCal would translate better to a sequential Java style program than raw TLA+ would.
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.
I've debated trying to write a PlusCal->Java transpiler [1], and I haven't really ruled that out yet; while I don't think it should be necessary to have that for PlusCal to be useful, I think it would potentially sweeten the sales pitch.
[1] I think PlusCal would translate better to a sequential Java style program than raw TLA+ would.