There are quite a few projects that do formally prove the algorithm before its implementation, but most of them we don't have access to. The closest we can eas

There are quite a few projects that do formally prove the algorithm before its implementation, but most of them we don't have access to. The closest we can easily see is the code JPL uses on their rovers and the associated C coding standard (http://lars-lab.jpl.nasa.gov/JPL_Coding_Standard_C.pdf http://lars-lab.jpl.nasa.gov/JPL_Coding_Standard_C.pdf). That, and the rest of NASA's software was pretty much done entirely using a waterfall approach.