Right, whenever you try to use mathematics/logic to reason about the real world, you risk that some of your assumptions may be wrong. Every formally verified project will have some set of trusted assumptions. But hopefully this can still dramatically reduce software vulnerabilities---for example, systems more often fail because of bugs in the program logic than bugs in the x86 processor, so assuming a specification for the hardware and proving the program correct with respect to that should still be helpful.

(As an aside, hardware and compilers are actually comparatively tractable things to verify--the specifications are well-defined, and they are used by lots of clients so the effort to verify them pays off better. I think in the future, we are more likely to have unproven application programs running on top of proven compilers & hardware than the opposite.)