Perfect Developer [1] is another one not yet mentioned. You write and verify your "specifications" (program-parts to be verified) using a language called "Perfe

Perfect Developer [1] is another one not yet mentioned. You write and verify your "specifications" (program-parts to be verified) using a language called "Perfect" and generate C++, C#, or Java from that (SPARK Ada generator in progress). [1] http://www.eschertech.com/products/perfect_developer.php http://www.eschertech.com/products/perfect_developer.php