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>