<story><title>Formally Verified Software in the Real World (2018)</title><url>https://cacm.acm.org/magazines/2018/10/231372-formally-verified-software-in-the-real-world/fulltext</url></story><parent_chain></parent_chain><comment><author>tpaschalis</author><text>Second day in a row where HN frontpage features formally verified software!&lt;p&gt;If you&amp;#x27;re like me, and would like to get started, or just see what this is all about, the TLA+ homepage and video course (narrated by Leslie Lamport himself), is a nice resource [1].&lt;p&gt;In about half an hour you will have a brief understanding of what &amp;quot;formal specification languages&amp;quot; are, write and &amp;#x27;prove&amp;#x27; your first small program&amp;#x2F;spec. If you have another hour to spend, keep the cheatsheet [2] near you and follow through, you will write and &amp;#x27;prove&amp;#x27; more complex specs, plus you&amp;#x27;ll start thinking about systems in a more abstract way. Finishing up the video course you&amp;#x27;ll be able to start reading complex specs others have written, or write a spec for any algorithm you think is fun!&lt;p&gt;[1] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;lamport.azurewebsites.net&amp;#x2F;video&amp;#x2F;videos.html&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;lamport.azurewebsites.net&amp;#x2F;video&amp;#x2F;videos.html&lt;/a&gt;   
[2] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;lamport.azurewebsites.net&amp;#x2F;tla&amp;#x2F;summary-standalone.pdf&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;lamport.azurewebsites.net&amp;#x2F;tla&amp;#x2F;summary-standalone.pdf&lt;/a&gt;</text></comment>
<story><title>Formally Verified Software in the Real World (2018)</title><url>https://cacm.acm.org/magazines/2018/10/231372-formally-verified-software-in-the-real-world/fulltext</url></story><parent_chain></parent_chain><comment><author>jschwartzi</author><text>I have wanted to see a real-world use of seL4 in a safety-critical system since I heard about it 2 years ago. This is really impressive, and I&amp;#x27;m very happy to see this here.</text></comment>