How can we know that formal methods work? An important goal of formal methods is to prove the correctness of systems, either by automated or human-directed means. However, it seems that even if you can give a correctness proof, you may NOT be able to guarantee that the system will not fail. For example:


The specification may not model the system correctly, or a production system may be too complicated to model, or the system may be flawed inherently due to contradictory requirements. What techniques are known to test whether a specification makes any sense at all?
The proof process may be flawed too! Who knows that those inference rules are correct and legitimate? Furthermore, proofs can be very large, and how do we know that they do not contain errors? This is the heart of the critique in de Millo, Lipton, and Perlis's "Social Processes and Proofs of Theorems and Programs".  How do modern formal methods researchers respond to this critique?
At runtime, there are many nondeterministic events and factors that can seriously affect the system. For example, cosmic rays can alter RAM in unpredictable ways, and more generally we have no guarantees that hardware will not suffer Byzantine faults, which Lamport has proved are very difficult to be robust against. So the correctness of the static system does not guarantee the  system won't fail! Are there any techniques known to account for the fallibility of real hardware?
At present, testing is the most important tool we have for establishing that software works. It seems like it should be a complementary tool with formal methods. However, I mostly see research which is either focused on formal methods or testing. What is known about combining the two?
Regarding 4: There's plenty of work combining formal methods and testing. Googling "formal methods testing" reveals quite a large amount of work. Although there are many different goals of such work, one of the key goals is to generate more effective test suites. This talk gives a nice introduction, based on model checking.

Also regarding the issue software security, which has been edited out of the question: formal methods need to work harder to deliver in that realm. Typically one writes a specification for a piece of software and verifies that the specification is satisfied, namely, that when the input satisfies the precondition that the output satisfies the postcondition. To ensure secure software one also needs to check also that the software behaves sensibly for input that does not satisfy the precondition. (This is of course equivalent to setting the precondition to true for all input.) The space of all inputs is typically much larger than just well-formed input, but typically this is one place where even functionally correct software can be violated, simply by violating its assumptions.

Regarding point 3: Some work has been done for verifying systems in settings where faults are explicitly modelled, including Faulty Logic:  Reasoning About Fault-tolerant Programs. Matthew Meola and David Walker. European Symposium on Programming, 2010. Work on probabilistic model checking and probabilistic verification certainly both also address the issue of faults to some degree.