Are there systems or is there software out there that is developed with a proof of correctness to back it up? Or are all critical systems developed merely with an aggressive code review and test cycle?
Coding for high integrity applications, in the real world, generally involves jumping through a bunch of QA hoops. Sometimes these hoops actually have something to do with getting the software right.
The medical device industry in the USA is regulated by the FDA. They publish a bunch of regulations covering "design", which includes all the software development. These regulations are basically ISO 9000 on steroids. You have to have a bunch of documents which are written, marked up by reviewers, updated with the review comments and signed off by a senior manager. Because the regulations are backed by law the FDA want to see evidence that these records have not been tampered with, for instance by writing the "expected result" of a test after you saw what result the test gave. So you either have to have a locked down totally secure CM system, or it all has to be signed and dated on paper (including the source code). The FDA inspectors have real law enforcement powers; if they see fit they can inspect your source code with an armed federal marshal. However they are not software specialists: their job is not to judge the quality of your code, just to make sure you have complied with all the regulations.
The aviation industry has to follow DO-178B, which is also ISO-9000 on steroids. You have to produce lots of documents and demonstrate traceability between them. I don't know if the FAA has the same approach to QA as the FDA though.
The problem is that nobody really knows how to produce software that does what it is supposed to. So instead we have a kind of cargo cult approach where we produce lots of documentation in the hope that this will imbue our software with quality. Its true that quality software generally has clear requirements and a simple logical architecture, but that doesn't mean that writing a "Requirements Document" or an "Architecture Document" will improve matters.
The evidence suggests that factor with the biggest impact on code correctness is the team that created it. However you can't write a legal constraint on a team. So instead the people with the job of mandating quality have to write constraints on process instead, in the vague hope that this will have a similar effect.