Alleged "microkernel mathematically proven to be bug free"

Georgi Guninski guninski at guninski.com
Mon Jul 28 08:26:50 PDT 2014


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).



More information about the cypherpunks mailing list