Comment by tkz1312

Hmm, but

> The multicore kernel uses a big-lock approach, which makes sense for tightly-coupled cores that share an L2 cache. It is not meant to scale to many cores,

I guess https://github.com/seL4/l4v/tree/rt is the ongoing verification work for that