His main site he mentions at the end is learntla.com. That's a good tutorial for using a subset of it that will get stuff done without trying to read a bunch of books on heavier stuff. He and I both also recommend Alloy for a taste in formal methods or blueprints like fouc said since it's designed for beginners with good guides and tutorials. TLA+/PlusCal with its model-checker is better at modeling order of execution (esp concurrency/distributed) whereas Alloy's is focused on structure of your program. Finally, Design-by-Contract combined with property-based testing or AFL-style testing with properties/contracts as runtime checks is probably combo most applicable to most programming languages and situations. If you know conditionals, you can use DbC in a lots of situations.<p><a href="http://alloytools.org" rel="nofollow">http://alloytools.org</a><p><a href="https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html" rel="nofollow">https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...</a><p><a href="https://hillelwayne.com/post/pbt-contracts/" rel="nofollow">https://hillelwayne.com/post/pbt-contracts/</a>