@cwebber wait I’m actually interested in this, I think stuff like sel4 is really really cool and I’m suprised more work hasn’t been done on doing a full formally verified os