TBH, as cool as TLA+ is, the biggest issue I generally see with trying to use formal methods in practice is that you need to keep the specification matching the actual implementation. Otherwise whatever you've formally verified doesn't match what actually got built.
So formal methods may be used for extremely critical parts of systems (eg; safety critical systems or in embedded where later fixes cannot be readily rolled out) but they fail to make inroads in most other development because it's a lot of extra work.
I've always seen it as a tool for validating a design rather than an implementation.
On the other hand, how many million man hours are spent re inventing the wheel that could instead be spent contributing to a library of extremely well-specified wheels?
What do you think of embedding it in a formal system like Lean as a frontend?
Hillel Wayne wrote a post[0] about this issue recently, but on a practical level I think I want to address it by writing a "how-to" on trace validation & model-based testing. There are a lot of projects out there that have tried this, where you either get your formal model to generate events that push your system around the state space or you collect traces from your system and validate that they're a correct behavior of your specification. Unfortunately, there isn't a good guide out there on how to do this; everybody kind of rolls their own, presents the conference talk, rinse repeat.
But yeah, that's basically the answer to the conformance problem for these sort of lightweight formal methods. Trace validation or model-based testing.
[0] https://buttondown.com/hillelwayne/archive/requirements-chan...)
To be totally fair, my article is about the problem of writing specs when your product features could change week to week, whereas I think u/alfalfasprout is talking about regular updates to an existing system slowly bringing it out of sync with the spec. For the latter problem, yeah trace validation and model-based testing is the best approach we have so far.
Plus my Kayfabe system [0], which was partly inspired by Ron Pressler's article on trace validation:
0. https://conf.tlapl.us/2020/11-Star_Dorminey-Kayfabe_Model_ba...
why are the lower case L's in that document bolded? a different weight? Not sure what the right technical change term is for the visual difference but it was extremely noticeable immediately upon opening the document