These two are the common resources recommended for this sort of thing: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcp

These two are the common resources recommended for this sort of thing: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://concrete-semantics.org/ http://concrete-semantics.org/ Most work in the field is using Coq or HOL. The second one applies to seL4. I don't think it will help you understand it much given the complexity of that work. You might have better luck looking at Myreen's verifications of LISP 1.5 or CakeML in Isabelle/HOL. Or even their verification of HOL itself.