It's all definitely worth looking into. Anyone trying to start will find Wheeler's page [1] much more helpful. I also included a book [2] on using dependent types for certified programming. There's also a few examples after of verifications with [3] being pretty cutting-edge in automation & thoroughness. I think we need people to put together a single resource where newcomers can see the various approaches, tools, and practical examples of how to use them. Further, we need to research more on which tools give you the most bug hunting benefit with the least time and expertise. There's some research done already but everything in this field is scattered.

Another point came up in a similar discussion: we need to focus most of our energy on raising the baseline of correctness for the average programmer. This includes things such as automated test generation, design by contract, and better type systems. The developer should be able to specify his or her intention with the code while the type system or runtime catches most of the errors. Maybe we just need a version of BASIC/Pascal with Ada-like safety built-in or similar restrictions on certain constructs. Not sure of the specifics but this is an important problem to solve.

[1] http://www.dwheeler.com/essays/high-assurance-floss.html

[2] http://adam.chlipala.net/cpdt/

[3] https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/hard...

[4] http://se.inf.ethz.ch/people/morandi/publications/prototypin...

[5] http://compcert.inria.fr/compcert-C.html

[6] http://repository.readscheme.org/ftp/papers/vlisp/guide.pdf

[7] http://research.microsoft.com/pubs/122884/pldi117-yang.pdf