Admittedly, the theory (or practice) of robust software design in critical-impact apps is not an area where I should try to assert any sort of personal expertise. I'll shut up now.

You're doing at least as good as the "experts." Besides, as my good friend Francis always said truth comes sooner out of error than confusion :).

You raise a good point about the specifications as well. Perhaps a problem well stated is indeed a problem half solved here. It appears to me that a proper tool for such a job would have to effectively generate tests to cover each set of possible errors introduced by the source code. It would not be possible to create all the tests by hand, that would only transfer the problem from the instructions to the tests.

Anyone have any thoughts/information on self-verifying languages? Is there a different term for them I'm missing? ("self-verifying programming language" turns up nothing in google).