To derive a program means to write a formal specification, which is usually non-executable, and then apply mathematically correct rules in order to obtain an executable program satisfying that specification.
The program thus obtained is then correct by construction.
The approach usually taken in formal verification is to first write a program, and then provide a proof that it conforms to a given specification.
The Bird-Meertens Formalism is an approach to program derivation.
Approaches to achieving correctness in Distributed computing include research languages such as the P programming language.