They make models of the software before writing any code, and a lot of the code can be generated from the models. There's a guarantee that if the model is correct so is the code. Or, you don't have to check that your hand-written C actually matches the system you were building.