Comment by throwawaymaths
Comment by throwawaymaths 3 days ago
> SeL4 is safe because of its extensively verified codebase written in a language suited for verification
I think this is incorrect. It is written in C, compiled to arm assembly, and the assembly is analyzed and checked by Isabelle/HOL.
You may be right, I was under the impression that the Haskell version was the verified version.