This is not necessarily true when it comes to formal verification.
Isn’t Risc-V only an instruction set specification, it is not a specification that describes the implementation of a chip. It is a good start, but in the end we also need an open-source implementation of a Risc-V CPU.
Very cool project. And the open-source Risc-V implementation they use is https://github.com/SpinalHDL/VexRiscv
That’s fine and commendable, but currently unachievable.
Consider the boundary between trust and verify. What you can verify you do not have to trust - as you say. Purism makes so much information available that you can verify a lot, so you have to trust a little. Most other companies are the exact opposite - allow you to verify a little or nothing, so you have to trust a lot.
While I hate the Intel ME (homunculus CPU) as much as the next guy, don’t lose sight of the fact that if you choose to distrust Intel then your Intel x86 computer would be worthless even if it did not have the homunculus CPU at all. The backdoor can be in the main CPU (either in its microcode or baked into the silicon). From that perspective, ARM is in practice not much better.
Depends what you mean by “compromised” but obviously another entity may actually be (vastly) superior to you in terms of either avoiding penetration or avoiding unintentional bugs - but you still have to trust that their intentions are to avoid those things.
If you like verifiability you should read about seL4. https://sel4.systems/ What do you think about that project?