How can we know that formal methods work?
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.