I have worked with quite rigorous design guidelines in embedded aerospace software. E.g. there was a 100+ page word document describing, in detail, the function

I have worked with quite rigorous design guidelines in embedded aerospace software. E.g. there was a 100+ page word document describing, in detail, the functioning of the software, down to a "if this, then that, within x amount of time". I would have loved to have a formal specification of this, not just to have my code checked, but also to make sure the specification is coherent. The problems with that were: - The cost of creating that specification would have been very substantial, both in money and in time. - The end to end functionality of the system was verified anyway and could not have been replaced by a formal correctness proof. Creating a few more test cases is cheap, creating a formal verification is extremely hard. Tye regulator expects that verification, it does not expect a formal proof. This is actually a project risk. - The people writing the specification do not think formally, they concern themselves with overall functionality, which they them translated into a more detailed description. There is a serious communication problem here if you want formal verification. I really like the concept, but to apply it you need to integrate it from ground up and rethink how you write software.