Formally verifying software takes much more time than just writing it, perhaps a factor of 10. For instance, the seL4 project[1] states that they used 2.2 perso

Formally verifying software takes much more time than just writing it, perhaps a factor of 10. For instance, the seL4 project[1] states that they used 2.2 person-years to write the kernel itself, and 20 person-years on the proof. Apparently the version of CompCert from 2007 (before any optimizations) took 2 person-years to write[2]. But some of those persons were pretty impressive. [1] http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf [2] http://memocode.irisa.fr/2007/leroy-compcert-memocode07.pdf http://memocode.irisa.fr/2007/leroy-compcert-memocode07.pdf