Keep in mind: 1. a non-verified approach can have many problems in the (informal) specification + implementation errors 2. the verified approach is likely to

Keep in mind: 1. a non-verified approach can have many problems in the (informal) specification + implementation errors 2. the verified approach is likely to have less specification errors (because the specification had to be formally written out and matched against an implementation) and implementation errors with respect to the specification will be almost impossible (minus faults in the compiler, OS and hardware). There's a huge jump in security guarantees between 1 and 2.