Check out the Alloy model checker. Simple with GUI, too. One guy I know says he just uses it like SQL. Hillel Wayne just published Practical TLA+. It helps with

Check out the Alloy model checker. Simple with GUI, too. One guy I know says he just uses it like SQL. Hillel Wayne just published Practical TLA+. It helps with concurrency and distributed systems. There's the book on SPARK Ada which lets you do system code that's provably safe. Finally, the easiest method to use in any language is Design-by-Contract. https://www.betterworldbooks.com/product/detail/Practical-TLA---Planning-Driven-Development-9781484238288 https://www.betterworldbooks.com/product/detail/Practical-TL... https://www.betterworldbooks.com/product/detail/Building-High-Integrity-Applications-with-SPARK-9781107656840 https://www.betterworldbooks.com/product/detail/Building-Hig... https://hillelwayne.com/post/pbt-contracts/ https://hillelwayne.com/post/pbt-contracts/