On 23 Jan 2018, at 11:38, Jeff Waugh <jdub@bethesignal.org<mailto:jdub@bethesignal.org>> wrote: Hi seL4 friends, Any thoughts and/or feelings about the Hyperkernel paper from SOSP'17? This paper describes an approach to designing, implementing, and formally verifying the functional correctness of an OS kernel, named Hyperkernel, with a high degree of proof automation and low proof burden. https://homes.cs.washington.edu/~helgi/papers/hyperkernel.pdf Indeed (you’ll find yours truly credited as the shepherd of the paper, which implies I reviewed it ;-) The high-level summary: It’s an impressive achievement to do this verification in a fully automated way (“only” 8 years after we did it manually in seL4 ;-) Unlike seL4, which was designed for real-world use from Day 1, hyperkernel is a toy system, and the approach doesn’t scale to non-toys. This is a consequence of their “finiteness” requirement. The same approach won’t work for seL4 (despite seL4’s simplicity). Gernot