<story><title>The seL4 microkernel</title><url>https://github.com/seL4/seL4</url></story><parent_chain></parent_chain><comment><author>gioele</author><text>Please note that the formally proven model has been implemented also in Haskell, not only in C.&lt;p&gt;Formally-proven-correct code + Haskell + literate programming = &lt;a href=&quot;https://github.com/seL4/seL4/blob/master/haskell/src/SEL4/Kernel/Thread.lhs&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;seL4&amp;#x2F;seL4&amp;#x2F;blob&amp;#x2F;master&amp;#x2F;haskell&amp;#x2F;src&amp;#x2F;SEL4&amp;#x2F;Ke...&lt;/a&gt;</text></comment>
<story><title>The seL4 microkernel</title><url>https://github.com/seL4/seL4</url></story><parent_chain></parent_chain><comment><author>Intermernet</author><text>seL4 is &amp;quot;The world&amp;#x27;s first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement&amp;quot; originally developed (as far as I know) at UNSW, further developed at NICTA.&lt;p&gt;The original project home page is at &lt;a href=&quot;http://ssrg.nicta.com.au/projects/seL4/&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;ssrg.nicta.com.au&amp;#x2F;projects&amp;#x2F;seL4&amp;#x2F;&lt;/a&gt; and the new page is at &lt;a href=&quot;http://sel4.systems/&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;sel4.systems&amp;#x2F;&lt;/a&gt;&lt;p&gt;Downloads at &lt;a href=&quot;http://ssrg.nicta.com.au/software/TS/seL4/&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;ssrg.nicta.com.au&amp;#x2F;software&amp;#x2F;TS&amp;#x2F;seL4&amp;#x2F;&lt;/a&gt;</text></comment>