[AnimalMuppet]

Maybe I lack vision in such matters, but: how would you corrupt the stack without an out-of-bounds write?

But there's another aspect that I think you missed: use after free.

As you say, achieving this level of soundness with C is hard. Proving it is much harder. (Except, how do you know you've achieved it if you don't prove it?)

[GoblinSlayer]

I suspect seL4 could be proven correct only because it uses simple lifetime patterns.