Good point. But choose the wrong hardware and you can never have provably correct software. E.g., the Intel x86 ISA makes all x86 processors impossible to prove correct. (there are 2^120 possible instruction encodings - the universe will die heat death before anyone could verify all of them in an implementation http://www.emulators.com/docs/nx06_rmw.htm )
Shrug. We have provably validated diodes AIUI. If you can get provably correct basic components you can build up complex components using the same techniques as in software.