news: http://www.theregister.co.uk/2014/07/28/aussie_droneprotecting_hackerdetecting_kernel_goes_open_source/ site: http://sel4.systems/ AFAICT they used Isabelle for the proofs. Coq sucks much (not counting its developers).