You still extend trust - in this case to the RISC-V foundation. (We're not even scratching the surface on the fact that the Coq proofs do not, IIUC, cover side channels)

At some point, you have to trust somebody - "build from first principles" is really only available for extremely well-funded players.

Also: "the specification must be out-of-synch with software expectations somehow". I see the hardware world hasn't changed at all :)