"As the OpenBSD devs will tell you, there have only been two known vulnerabilities in default OpenBSD installs in the history of OpenBSD. This strongly suggests that having decent software quality is an effective way to prevent vulnerabilities from existing in the first place."

I addressed that myth in my main comment. See here:

http://pastebin.com/6cW3FyJE

They just assess and count differently than most folks. ;)

" If we put half the effort we put into palliative defense measures into formal verification or doing things right the first time, I suspect it would be drastically more effective."

I agree being on side of high-assurance security. OpenBSD doesn't so I don't know your statement supports what they do. They systematically avoid formal verification like what you described, safer languages, coding styles for static analysis, etc. It's people from my side of things promoting or building on those. They just hunt bugs in C code by eye and hope their probabilistic mitigations always work. Totally different.