I've been a big nerd for formal methods for quite awhile, and have been broadly unsuccessful in getting employers onboard.

I have pretty cynical opinions as to the "why" of this, largely involving the fact that the vast majority of software engineers refuse to learn anything that they weren't explicitly taught in college, but regardless of the reason whenever I have tried proposing TLA+ in the past, people will nod along and wait for me to stop talking. I've had several managers say "they'll look into it", which was such an obvious lie that I don't know why they even bothered.

I've "snuck in" TLA+ usage a few times. I gave up on getting anyone else to use TLA+, but as I've gotten more senior-level, I have been given a fair bit more leeway on how I approach projects and as such I have been able to budget myself a day or two to model some of the less-obvious bits of concurrency.

All that said, I have had some luck with designing stuff with TLA+, then feeding the spec into Claude and getting that to implement the actual executable code. Maybe I'll be able to convince an employer that's a good use of time now.

Software engineers are rarely engineers at all, and pretty much never know anything about computer science.

> I have pretty cynical opinions as to the "why" of this, largely involving the fact that the vast majority of software engineers refuse to learn anything that they weren't explicitly taught in college, but regardless of the reason

I think it's not only SWEs, but general persons that goe to college primarily to get a job, without having a natural curiosity for things.