3 ms·

I understand CertiKOS used Coq so the verification was at least half-automated? How L4 was certified -- what were the tools available at the time? Verification

I understand CertiKOS used Coq so the verification was at least half-automated? How L4 was certified -- what were the tools available at the time? Verification still remains huge work but sounds less heroic nowadays. Now that we have tools and methodologies for verification, the announce of yet another secure OS suddenly sounds much less impressive.

sanxiyn 10y ago
Here is seL4 proof: https://github.com/seL4/l4v https://github.com/seL4/l4v To quote, "Most proofs in this repository are conducted in the interactive proof assistant Isabelle/HOL".