Let me address now a number of different contrasts, I have mentioned already. Is it possible absolute reliability? Well, here some kind of misclaimer has to be made.
Complete certainty is utopian, formal methods can only increase our confidence, because at best we can only prove formally that a given piece of software meets its formal specifications.
The exact correspondence between the specification and the system can be checked, but the correspondence between the specification and the real world can not be made formal in any possible sense.
This has to be achieved on the basis of different tools from formal methods, and indeed this can be a problem sometimes, but this is a problem that of course at this stage we can not address.