Can the seL4 proofs handle recursive functions?

We are writing some code for the seL4_libs where a recursive function makes the most sense. I know that part of the code is not verified, but it got me curious as to whether the seL4 proofs could handle recursive functions.

It can, yes.

The more abstract proof levels in Isabelle/HOL make natural use of recursion all the time (lists etc), and the C level also supports recursion. There is even an in-kernel function that is nominally recursive that makes use of that; the maximum recursion depth in that case is only 3, but it looks as recursive to the verification environment as a “real” recursive function.