There's actually been a lot of work in that going back five years or so. Here's a commercialized one:

http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf

Formal verification of specs, microcode, and security policy they hold in ACL2. Part of that is embedding a separation kernel a la MILS or SKPP model. It also has triplicated registers for fault-tolerance. Then, they integrate high-level languages like SPARK and microCryptol with that using certified compilers or equivalence checking.

Here's some examples from CompSci work:

https://eprint.iacr.org/2016/846.pdf

http://users.ece.utexas.edu/~tiwari/pubs/tiwari-dissertation...

http://cs.ucsb.edu/~sherwood/glift/

http://ieeexplore.ieee.org/document/7927266/

http://www.eecs.ucf.edu/~jinyier/papers/VTS12.pdf

http://www.cse.psu.edu/~dbz5017/pub/asplos17.pdf

Just also found a super-old one that tries to do it with capability-based mechanisms.

https://dl.acm.org/citation.cfm?id=803030

Most hardware work in information-flow analysis and control is currently focused on making hardware that controls bad software. I don't think most of them consider a CPU failure. If anything, they might be more vulnerable from a practical strategy of trying to reuse existing cores by making info-flow components that operate side-by-side with them. Here's an example from that area, though, since they could be modified to address recent concerns.

http://www.crash-safe.org/assets/verified-ifc-popl2014.pdf

http://csl.stanford.edu/~christos/publications/2010.hari_kan...