<story><title>Logipedia – Encyclopedia of Formal Proofs</title><url>http://logipedia.inria.fr/</url></story><parent_chain></parent_chain><comment><author>YorkshireSeason</author><text>How does this relate to the &lt;i&gt;Archive of Formal Proofs&lt;/i&gt; [1] and &lt;i&gt;Mizar&amp;#x27;s Mathematical Library&lt;/i&gt; [2]?&lt;p&gt;[1] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;www.isa-afp.org&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;www.isa-afp.org&amp;#x2F;&lt;/a&gt;&lt;p&gt;[2] &lt;a href=&quot;http:&amp;#x2F;&amp;#x2F;mizar.org&amp;#x2F;library&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;mizar.org&amp;#x2F;library&amp;#x2F;&lt;/a&gt;</text></comment>
<story><title>Logipedia – Encyclopedia of Formal Proofs</title><url>http://logipedia.inria.fr/</url></story><parent_chain></parent_chain><comment><author>agentultra</author><text>Oh very good!&lt;p&gt;I started a repository for TLA+ modules years ago that I was hoping would turn into something like this [0]. Like many projects I never took it very far but I&amp;#x27;ve been using formal methods in practice for a couple of years now, might be worth revisiting...&lt;p&gt;[0] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;agentultra&amp;#x2F;software-spec-library&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;agentultra&amp;#x2F;software-spec-library&lt;/a&gt;</text></comment>