For embedded and security applications this is extremely important and there's already tons of work done in this field - for example sel4 (https://sel4.systems/

For embedded and security applications this is extremely important and there's already tons of work done in this field - for example sel4 (https://sel4.systems/ https://sel4.systems/), ivory/tower (https://ivorylang.org/ https://ivorylang.org/), yosys (http://www.clifford.at/papers/2016/yosys-synth-formal/slides.pdf http://www.clifford.at/papers/2016/yosys-synth-formal/slides...) for FPGAs.