You should look into RISC-V as well. Someone posted something about a formally-verified OS that runs on an fpga emulation of risc v. it’s called lion. Super interesting stuff and some among us figure it could be a foundation for an end-to-end formally verified machine. Perhaps virtually zero attack surface area…