I've been wondering recently to what extent formal verification could be used to simplify CPU hardware and ISAs. For example, MMUs are unnecessary if the OS verifies that all programs only access memory that's been allocated to it. This paper[0] seems to imply that the savings would be non-negligible. Also interrupts and context switching could be avoided if programs are cooperatively scheduled and verified that they always yield after an appropriate amount of time.
Those two examples are the only ones I could come up with, but I suspect that's because I don't know very much about hardware design. Are people working on this or am I just off-base here?
Check out theseus! It's exploring some of these ideas.
https://github.com/theseus-os/Theseus