I find it interesting that there is no mention of using dependently typed languages or proof engines for this application. Something like Coq, where you write the formal proof of correctness as you write the program, would fit the bill nicely if you really care about safety over ease of implementation.