Some recent happenings in Cryptol land include:<p><pre><code> * Dylan recently released a literate Cryptol version of the CFRG's ChaCha20/Poly1305 document. Very cool to see more Cryptol code like this.
* Merged the fork of SBV with upstream.
* ABC is now a supported prover.
* Support for parallel (first to finish) proving using ':set prover=any'.
* The type checker has been revamped for v2.3, so we should see simpler constraints "soon".</code></pre>
It's another amazing piece of work largely developed by Galois Inc: a company that invents and develops great stuff on a regular basis. One of the few doing high assurance. Their blog [1] is a gold mine of their interesting work and tips.<p>Two other works HN readers might like are Copilot [2] and Ivory [3]. Copilot is a DSL for distributed monitors and real-time systems. The result is QuickCheck'd, model-checked, hard, real-time C. Ivory is a DSL that embeds a subset of C into Haskell to leverage its power and increase safety. It was used in the SMACCMPilot UAV program [4], which is open source.<p>[1] <a href="https://galois.com/blog/" rel="nofollow">https://galois.com/blog/</a><p>[2] <a href="http://leepike.github.io/Copilot/" rel="nofollow">http://leepike.github.io/Copilot/</a><p>[3] <a href="http://ivorylang.org/ivory-introduction.html" rel="nofollow">http://ivorylang.org/ivory-introduction.html</a><p>[4] <a href="https://galois.com/blog/2013/10/smaccmpilot-open-source-autopilot-software-for-uavs/" rel="nofollow">https://galois.com/blog/2013/10/smaccmpilot-open-source-auto...</a>
Cryptol was originally designed for the NSA. There's a good article on it in NSA's The Next Wave from 2011 [1], which is also linked under documentation.<p>[1] PDF: <a href="https://www.nsa.gov/research/tnw/tnw191/articles/pdfs/TNW_19_1_Web.pdf" rel="nofollow">https://www.nsa.gov/research/tnw/tnw191/articles/pdfs/TNW_19...</a>