I have tried to use Coq and Frama-C to prove commercial OCaml and C programs, without, it has to be said, any success. I'm waiting for someone to write the brilliant tutorial.
Research tools are getting closer to what people consider "real" programs, even if they often focus on embedded systems software. CompCert already deals with a quite large subset of C. Frama-C can deal with most if not all syntactic features of C, but then the next challenge is the C standard library, e.g. specifying every useful function (and even "simple" ones such as memcpy can be quite tricky). Afterwards, you have to deal with the glibc, then other high-level libraries, etc...
Most of these tools are either still in a mostly-academic setting (where "documentation = conference paper"), or do not have enough funding to pay for the development of more user-friendly features and extensive documentation. But with the ever-increasing security issues receiving media attention lately, we can hope more funding will allow these tools to reach a more mainstream status.
By the way, could you give an example of a small program that you would consider "real"? Just to have an idea of its size and complexity.
Firstly I don't expect to prove a whole program. However being able to prove the correctness of key functions or algorithms in a program could be useful.
You mention glibc, and it would be great to prove that (for example) 'qsort' is correct. That wouldn't be entirely trivial:
For an example of a larger program, I'd like to prove various invariants of C programs, such as that 'reply_with_error' is called exactly once on every error path in this program:
