I think we're more likely going to see formally verified software development frameworks...something like a "verified Rails" before we see programmers using proof-checking in the general case. Basically it'll be the model-checking software built into a framework and a tool that will tell you if your code plays well / is safe according to the model or not.
Having programmers use proof checkers to write proofs about their own software and then prove them is still very far away, if it'll ever happen at all. One can always dream happy dreams about the Curry-Howard Isomorphism, though.
Ur/Web uses dependent types (Ur) to build statically checked web libraries that prevent common bugs such as malformed or stale links. The exciting part (IMO) is that the 'row types' allow encoding your database schema in the type system, so it prevents bugs common to frameworks with heavy code generation, such as the ORM in Rails or template libraries in C++.
The connection to formal verification is that dependent types (depending on how you do them) let you stuff custom computations into the type checking phase. The two coolest uses of dependent types (IMO) are to verify your code and, surprisingly, synthesize boilerplate.
(Btw, the guy making Ur/Web is quite important in the Coq community and Ur is one of his research vehicles for these ideas.)
Having programmers use proof checkers to write proofs about their own software and then prove them is still very far away, if it'll ever happen at all. One can always dream happy dreams about the Curry-Howard Isomorphism, though.