HDLs can describe hardware behavior, and you can theoretically prove that a certain hardware design has the desired behavior, assuming you can also describe that desired behavior in a way that the prover can understand. Theoretically you could prove the full stack, but you still need to actually manufacture it at some point. Beyond physical decay, radation etc. like @Phlopsi mentioned, there are multiple steps between HDL and physical device where things can go wrong: you have to compile the HDL into gates, create a physical layout, create a set of masks, and deposit/etch/etc. your way to victory.
It's true there are tools (such as LVS) that reduce the risk of making errors at each stage in this chain. But (1) these tools, at the moment, still need people to drive them in the right direction, and any point where human discretion is involved is a possible point of failure; and (2) the tools themselves are not part of the system being proven, so you have to invent tools to prove the tools, etc... (also, the EDA tool industry regularly spits out garbage that makes Cyberpunk 2077 look like a model of software development by comparison, but that is neither here nor there)
At the end of the day you have to trust something, whether it's libc, the OS, the processor, the guy who wrote the simulator the processor was tested in... But all that stuff is outside the scope of what a programming language can help with.