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