I wish we could and I think we should.

I'm just very sad we don't have safe hardware w.r.t. memory corruption via rowhammer and I don't think any of the typical formal methods or seL4 account for it. Safely running untrusted code is nearly impossible on modern computers.