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:
