1. Yes, I did a deep dive into TLA+ (Hillel's publications are great for this) and used it as a proof of concept (attempted to convince the office to use it) to demonstrate the nature of a bug (I described how we thought the system behaved (per spec), no issues, then recreated the bug by selectively weakening the model, which mirrored exactly the problems in the real system). I've also used TLA+ as a model checker for non-programming systems to demonstrate where we could anticipate errors/problems and strengthen policy, physical, or software controls to prevent/mitigate them, that was a side project for me but the information was used by my sister professionally. That worked well because real world systems are inherently concurrent. It was another case of trying to convince management that simulation/modeling was good (it worked in her case, to some extent).
2. Some of it, not all of it. (1) was a concurrency issue and was well-suited to TLA+'s approach. Present office does not deal with concurrency to the same extent so I wouldn't try to sell TLA+ here. Other methods would be more appropriate (especially things like proper state diagrams/statecharts which are amenable to simulation, versus the traditional prose version of software specifications). These are lightweight formal methods or spec-centric formal methods that don't necessarily require heavy proofs to gain a benefit from them. Since most of the errors I've encountered fall into two camps: straight up logic errors (verification should catch) and specification errors (validation should catch). My focus has been on the latter. I think testing in general catches the former pretty well, or using a language that lets you code out a lot of logic errors, but specification errors are hard-to-impossible to catch until you place the product in front of the customer. Applying formal methods + simulation & modeling to the specification can really help here, even if it's only to subsets of the spec, as you can test against that verified/validated specification more effectively than against a prose specification (what I usually see in my work, 1k+ documents that are largely self-contradictory).
3. See 1. I did that on my own, but it was intended to start a conversation in the office about modeling our systems more formally to gain similar insights elsewhere (and better understand the system design). It did not take off.
4. People don't want to learn the methods, especially in legacy systems (which I demonstrated at my previous office would benefit from formal methods). There's also confusion over what formal methods bring you. I had to repeatedly state that I wasn't going to prove that our system worked correctly (in the sense of proving theorems about the code or something), but only properties of the specification (which for most systems were 1k+ page documents). Without a compelling case study, you will not convince a harried office that it's worth investing in something that seems slow ("Why aren't you coding!?!"), even if it does ultimately save time (once you start coding you can more directly implement the feature or have a better idea of what/how to test).
Comments
1. Yes, I did a deep dive into TLA+ (Hillel's publications are great for this) and used it as a proof of concept (attempted to convince the office to use it) to demonstrate the nature of a bug (I described how we thought the system behaved (per spec), no issues, then recreated the bug by selectively weakening the model, which mirrored exactly the problems in the real system). I've also used TLA+ as a model checker for non-programming systems to demonstrate where we could anticipate errors/problems and strengthen policy, physical, or software controls to prevent/mitigate them, that was a side project for me but the information was used by my sister professionally. That worked well because real world systems are inherently concurrent. It was another case of trying to convince management that simulation/modeling was good (it worked in her case, to some extent).
2. Some of it, not all of it. (1) was a concurrency issue and was well-suited to TLA+'s approach. Present office does not deal with concurrency to the same extent so I wouldn't try to sell TLA+ here. Other methods would be more appropriate (especially things like proper state diagrams/statecharts which are amenable to simulation, versus the traditional prose version of software specifications). These are lightweight formal methods or spec-centric formal methods that don't necessarily require heavy proofs to gain a benefit from them. Since most of the errors I've encountered fall into two camps: straight up logic errors (verification should catch) and specification errors (validation should catch). My focus has been on the latter. I think testing in general catches the former pretty well, or using a language that lets you code out a lot of logic errors, but specification errors are hard-to-impossible to catch until you place the product in front of the customer. Applying formal methods + simulation & modeling to the specification can really help here, even if it's only to subsets of the spec, as you can test against that verified/validated specification more effectively than against a prose specification (what I usually see in my work, 1k+ documents that are largely self-contradictory).
3. See 1. I did that on my own, but it was intended to start a conversation in the office about modeling our systems more formally to gain similar insights elsewhere (and better understand the system design). It did not take off.
4. People don't want to learn the methods, especially in legacy systems (which I demonstrated at my previous office would benefit from formal methods). There's also confusion over what formal methods bring you. I had to repeatedly state that I wasn't going to prove that our system worked correctly (in the sense of proving theorems about the code or something), but only properties of the specification (which for most systems were 1k+ page documents). Without a compelling case study, you will not convince a harried office that it's worth investing in something that seems slow ("Why aren't you coding!?!"), even if it does ultimately save time (once you start coding you can more directly implement the feature or have a better idea of what/how to test).