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 Thanks, Jeff