High-assurance sub-fields have many examples where the code is easiest part as it's just implementing a verified spec. Others have plenty of work on both sides. Altran (formerly Praxis) is a nice example with many commercial successes:

http://sdg.csail.mit.edu/6.894/dnjPapers/hall-correctness-by...