Alloy, mostly used for modeling and analysis but see the program verification section about halfway down this very long page: https://alloytools.org/citations/

Alloy, mostly used for modeling and analysis but see the program verification section about halfway down this very long page: https://alloytools.org/citations/case-studies.html https://alloytools.org/citations/case-studies.html Linked at the top of that page is a book about Alloy. There is also a book about TLA, mentioned in another comment here.