I said that about TLA+'s model checking. With things like Verasco, I figured a verified model checker could be done. As usual, I also searched for examples with

I said that about TLA+'s model checking. With things like Verasco, I figured a verified model checker could be done. As usual, I also searched for examples with SPIN since (a) they're used for similar things and (b) more people used SPIN in the past. Found this: https://www21.in.tum.de/~lammich/pub/nfm2016_por.pdf https://www21.in.tum.de/~lammich/pub/nfm2016_por.pdf Lammich was a name I recognized immediately for his work converting functional data structures to imperative ones in Isabelle/HOL. He and his collaborators have done quite a few interesting things so I'll just leave you the whole list: https://www21.in.tum.de/~lammich/ https://www21.in.tum.de/~lammich/ Far as lightweight methods, I recently summarized some recommendations with supporting case studies on Schneier's blog based on a message I sent someone trying to sell management on verification. It's a draft that I'm getting feedback on from various people rather than something I'm 100% solid on. The SPARK work combined with their book is still one of easiest methods in terms of automation achieved for covering specific properties that are often significant. https://www.schneier.com/blog/archives/2018/02/friday_squid_bl_612.html#c6769756 https://www.schneier.com/blog/archives/2018/02/friday_squid_...