In the wild what is more common in my experience is to use a formal specification language like Z or Object-Z and then recreate the the program in a "normal" language using pair programmers and/or extensive code review to attempt to ensure it conforms to the specification. While not perfect, for critical things this approach is far more time consuming and less bug prone than typical development.

I have also seen limited attempts at writing code generators that take Object-Z specifications as input. My understanding is that this is an area of ongoing research, but even a program that generates code for a subset of a Object-Z specification can save a lot of time.

Example research: http://www.jot.fm/issues/issue_2008_11/article6.pdf