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