<story><title>Modeling Redux with TLA+</title><url>https://www.hillelwayne.com/post/tla-redux/</url></story><parent_chain></parent_chain><comment><author>nickpsecurity</author><text>His main site he mentions at the end is learntla.com. That&amp;#x27;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&amp;#x27;s designed for beginners with good guides and tutorials. TLA+&amp;#x2F;PlusCal with its model-checker is better at modeling order of execution (esp concurrency&amp;#x2F;distributed) whereas Alloy&amp;#x27;s is focused on structure of your program. Finally, Design-by-Contract combined with property-based testing or AFL-style testing with properties&amp;#x2F;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.&lt;p&gt;&lt;a href=&quot;http:&amp;#x2F;&amp;#x2F;alloytools.org&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;alloytools.org&lt;/a&gt;&lt;p&gt;&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;www.win.tue.nl&amp;#x2F;~wstomv&amp;#x2F;edu&amp;#x2F;2ip30&amp;#x2F;references&amp;#x2F;design-by-contract&amp;#x2F;index.html&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;www.win.tue.nl&amp;#x2F;~wstomv&amp;#x2F;edu&amp;#x2F;2ip30&amp;#x2F;references&amp;#x2F;design-b...&lt;/a&gt;&lt;p&gt;&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;hillelwayne.com&amp;#x2F;post&amp;#x2F;pbt-contracts&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;hillelwayne.com&amp;#x2F;post&amp;#x2F;pbt-contracts&amp;#x2F;&lt;/a&gt;</text></comment>
<story><title>Modeling Redux with TLA+</title><url>https://www.hillelwayne.com/post/tla-redux/</url></story><parent_chain></parent_chain><comment><author>mettamage</author><text>Sidenote: I remember that my teacher Maarten van Steen (who taught distributed systems at my university) talked about Leslie Lamport and I remember that he started TLA+. If you don&amp;#x27;t know about any of this, I invite you to take a look.&lt;p&gt;Background info on Lamport [1]. Maarten van Steen offers his book for free on distributed systems. See [2].&lt;p&gt;1. &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;en.wikipedia.org&amp;#x2F;wiki&amp;#x2F;Leslie_Lamport&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;en.wikipedia.org&amp;#x2F;wiki&amp;#x2F;Leslie_Lamport&lt;/a&gt;&lt;p&gt;2. &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;www.distributed-systems.net&amp;#x2F;index.php&amp;#x2F;books&amp;#x2F;distributed-systems-3rd-edition-2017&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;www.distributed-systems.net&amp;#x2F;index.php&amp;#x2F;books&amp;#x2F;distribu...&lt;/a&gt;</text></comment>