[TheCoelacanth]

It seems pretty useless to even try to formally verify a program when all of the dependencies that are necessary to do anything useful are not formally verified. Where do I find a formally verified TCP/IP stack, a formally verified database, a formally verified HTML/CSS renderer, etc.?

[catnaroek]

Even if your dependencies are not formally verified, it is useful to formalize your expectations of them.

[tehwalrus]

I've found unit tests for system libraries like this before. The idea is that you run them each time you upgrade your framework, but in practise you run them every time (slowing down your debug loop) and managers use them to inflate the effectiveness of your actual tests, which is obviously measured in "number of unit tests" rather than %coverage (or, better still, %possible input values to each line)

[catnaroek]

Unit tests don't constitute “formalization” by any stretch of the term's meaning.

[tehwalrus]

Sorry, I proposed unit testing as a real-world formalisation of requirements in an earlier post, and you didn't contradict me. What automated system would you use for this instead?

[catnaroek]

Automated, huh? There is no replacement for using your brain, and reasoning abstractly about the preconditions and postconditions of program fragments.

[tehwalrus]

So, you write down the formal requirements you have of an operating system (with aggressive auto-updates enabled, or disabled, as the customer chooses) once, on a piece of paper, and hope that they don't change?

Your method seems impractical in the extreme in a commercial team environment.