Hmmm, one problem I see with this, at least for us open source mortals, is that all this rigor sits atop a festering pile of C, that is, the GCC (the GNAT Ada c

Hmmm, one problem I see with this, at least for us open source mortals, is that all this rigor sits atop a festering pile of C, that is, the GCC (the GNAT Ada compiler in it).... At least as these people are using SPARK/Ada. Then again, maybe I should return to looking at Intel CPU and chipset errata.... On the third hand, these guys aren't using systems with ECC.... (http://ark.intel.com/products/64893/intel-core-i7-3520m-processor-4m-cache-up-to-3_60-ghz http://ark.intel.com/products/64893/intel-core-i7-3520m-proc...).