I can think of one more trustworthy alternative: formal verification. seL4 is a formally verified microkernel [1]. There are formally verified compilers [2] a

I can think of one more trustworthy alternative: formal verification. seL4 is a formally verified microkernel [1]. There are formally verified compilers [2] and web browsers [3]. And formally verified formal verifiers. :-) [1] http://ssrg.nicta.com.au/projects/seL4/ http://ssrg.nicta.com.au/projects/seL4/ [2] http://compcert.inria.fr/ http://compcert.inria.fr/ [3] http://goto.ucsd.edu/quark/ http://goto.ucsd.edu/quark/