Can we prove termitation of every kernel entry? Clearly not including
assembly. But the Hyperkernel[1] is a good example of how SMT solvers
can go a long way in proving interesting properties.

I _may_ just be able to pull off using CBMC in the syscall entry path
as long as I create reasonable abstractions for linked lists (it won't
work with those).

[1] https://unsat.cs.washington.edu/projects/hyperkernel/