I'm currently working with very good researchers on formal verification of a part of the software I'm writing in rewriting logic with Maude - formalizing a fairly simplified version of the execution engine algorithms (0.005% of the c++ codebase maybe, 2500 lines of c++ at most) is taking ~a year roughly so far. That's not really viable for general development especially with requirements which evolve all the time.
