Formal program verification in practice
I'll try to give a succinct answer to some of your questions. Please bear in mind that this is not strictly my field of research, so some of my info may be outdated/incorrect.


There are many tools that are specifically designed to formally prove properties of Java and C++. 

However I need to make a small digression here: what does it mean to prove correctness of a program? The Java type checker proves a formal property of a Java program, namely that certain errors, like adding a float and an int, can never occur! I imagine you are interested in much stronger properties, namely that your program can never enter into an unwanted state, or that the output of a certain function conforms to a certain mathematical specification. In short, there is a wide gradient of what "proving a program correct" can mean, from simple security properties to a full proof that the program fulfills a detailed specification.

Now I'm going to assume that you are interested in proving strong properties about your programs. If you are interested in security properties (your program can not reach a certain state), then in general it seems the best approach is model checking. However if you wish to fully specify the behavior of a Java program, your best bet is to use a specification language for that language, for instance JML. There are such languages for specifying the behavior of C programs, for instance ACSL, but I don't know about C++.
Once you have your specifications, you need to prove that the program conforms to that specification.

For this you need a tool that has a formal understanding of both your specification and the operational semantics of your language (Java or C++) in order to express the adequacy theorem, namely that the execution of the program respects the specification.

This tool should also allow you to formulate or generate the proof of that theorem. Now both of these tasks (specifying and proving) are quite difficult, so they are often separated in two: 


One tool that parses the code, the specification and generates the adequacy theorem. As Frank mentioned, Krakatoa is an example of such a tool.
One tool that proves the theorem(s), automatically or interactively. Coq interacts with Krakatoa in this manner, and there are some powerful automated tools like Z3 which can also be used.


One (minor) point: there are some theorems which are much too hard to be proven with automated methods, and automatic theorem provers are known to occasionally have soundness bugs which make them less trustworthy. This is an area where Coq shines in comparison (but it is not automatic!).
If you want to generate Ocaml code, then definitely write in Coq (Gallina) first, then extract the code. However, Coq is terrible at generating C++ or Java, if it is even possible.
Can the above tools handle threading and performance issues? Probably not, performance and threading concerns are best handled by specifically designed tools, as they are particularly hard problems. I'm not sure I have any tools to recommend here, though Martin Hofmann's PolyNI project seems interesting.


In conclusion: formal verification of "real world" Java and C++ programs is a large and well-developed field, and Coq is suitable for parts of that task. You can find a high-level overview here for example.