If you want correctness, you need proofs, or generate the code from specification. And even then cosmic rays and bit-banging and faulty hardware can break your application. Or simple change of stack size :)