I agree. Formal methods is the best technology I know of that has a hope of eliminating a large class of security vunerabilities. Projects like seL4 have a lot of promise: small, formally verified kernels or virtualization layers that provide separation and provable security guarantees.