What about the more complex hardware such as the CPU? There are plenty of opportunities for mistakes there, some not so obvious (such as Spectre attacks). And I can't imagine you'd get away with completely isolating it like the memory.

My long term plan was actually to do a full formal verification of the CPU against the ISA spec and prove no state leakage between thread contexts, but I didn't have time to do that before I graduated

I deliberately went with a very simple CPU (2-way in order, barrel scheduler with no pipeline forwarding, no speculation or branch prediction) to minimize opportunities for things to go wrong and keep the design simple enough that full end to end formal in the future would be tractable. Spectre/Meltdown are a perfect example of attack classes that are entirely eliminated by such a simple design.

I was targeting safety critical systems where you're willing to give up some CPU performance for extreme levels of assurance that the system won't fail on you.

At what point does it become easier to formally verify the software than the hardware? Certainly it's easier to change the software than the hardware, so there is already incentive to not move things into hardware that need not be there.

Since software is so easy to change, nobody bothers verifying it. The more we put into software, the more room there is for cutting corners in testing because, "we can always send out a firmware upgrade later." Me, I'd rather go back to the old days when updates to hardware were expensive so you better get it right.

It's like writing with a ball pen vs a pencil. But you could be just as careful with a pencil. I'm just wondering if what you are proposing is the equivalent of runes.