[lambdaone]

It is, however, in principle possible to prove that a processor implements the spec and only the spec; seach for "formal verification risc v" to find out more.

Of course if someone can sneak a backdoor into the spec, all bets are off.

[hmry]

You would also need to prove that the physical processor in your hands was actually manufactured according to the verified design, and not a slightly different design with a back door added. Which is infeasible for all processors manufactured in the last 30 years.

[eschaton]

And even if you did this, which may in principle be possible, you still wouldn’t be able to prove that there aren’t any backdoors leveraging unexpected physical interactions between components.

For example, even if everything was provably manufactured to spec, it could be laid out in a way that exposes side channels, enables rowhammer-like attacks, and so on.