Is an axiomatically correct OS possible?

Let's take a completely hypothetical situation. Let's assume that we now have the physical technology to warp space and time. Of course, the calculations are going to be horrific, but we can get a computer to perform them. However, these calculations are incredibly critical, a single error and the entire universe never existed.

What we need is a computer which will never make a mistake. This idea was inspired by a consideration of the attempts of mathematicians to secure the foundations of maths to ensure that thousands of years of work by the most enlightened luminaries could be logically verified as being true.

Of course, this isn't available off the shelf. Microsoft's software is renowned for its buggyness, and the BSOD would not be welcomed in most critically important installations. Whilst some people might say "I trust my ass chip to Linux", it's your ass, not mine or the rest of the worlds.

So what we'd need is a creation, from the ground up, of a new computer system. The question is: where do you start? With something of this level of importance, everything needs to be considered. First, the hardware. It would be more than just embarrassing should a minor error in a lookup table (such as the Intel Pentium floating point error) caused the destruction of life as we know it. We'd need to be able to completely verify that the chip was correct and able to self-correct from random errors caused by background radiation. Of course, we'd run them 10-redundant, but if one has a bug, they'll all have it. Similarly, all the rest of the hardware would have to be correct - but this isn't the main part of my argument.

Let's assume we've got perfect hardware. Now we need to build a perfect OS. But what do we program it in? We can't use any previously existing language to start, as that programming language may introduce bugs. For example, a version of C that was hacked to automatically include its own source in any new version of C was at one point created. We'd have to rebuild from scratch, from sending bytes back and forth. But it is incredibly difficult to verify that that is correct... a major problem. We'd have to build an assembler to make the entry easier, and to build the perfect C, or someother programming language (maybe proprietry). Then we'd have to build the actual control program.

The major problem is that there is no culture of ensuring that a program is axiomatically correct. How would you go about doing such a difficult task? Naturally, the programming language would be built with large numbers of checks - but how do we ensure that it is definately, authoritavely correct? I ask the noders of the world to help.