An example of something you can formally verify with proofs in Software Development

Question

I have been working on understanding formal verification of software. Formal methods include things like modeling your software with Petri Nets, Automata, or State-Transition Graphs. Other techniques for formal verification include using type systems, model checking, automated theorem proving, proofs, and doing program derivation. Finally, there is testing, but I wont go into that here.

I have asked several questions regarding these topics:

• What to prove and how to prove it
• What you want to "prove" in algorithms
• High-level requirements for a Proof of "Saving to the Database"
• How to prove a function returns a value
• How proofs can be applied to a simple logging function
• How to prove a side effect in a function
• How to prove $c = a + b$ using Program Verification Techniques
• How to use Hoare Logic to Prove this Assertion
• How to apply Hoare Logic to this function
• How to apply Operational Semantics to this function

The gist of the answers is essentially, you can't apply formal proofs to realistic software applications. This is a bit disappointing to hear, especially when there are projects such as CompCert, the "formally verified" C compiler. My first question is, what exactly they mean (in CompCert) by "formally verified". Wondering which of the following (or something different) this includes:

• Model Checking
• Formal Proofs (e.g. Hoare Logic)
• Type Theory
• Transition Systems
• Operational Semantics / Denotational Semantics

My second question is, what is a realistic application of proofs to formally verify software (i.e. a web application example, not a textbook example). After asking these questions, I am discouraged that there are no applications of formal proofs to practical software development.

At first I thought that using Coq I could somehow write "formal proofs" for my code, and walk away with a sense of confidence that my code was "formally verified". But now I don't know if that has any practical or realistic meaning. That was what I was getting at in How to prove a function returns a value, High-level requirements for a Proof of “Saving to the Database”, and How proofs can be applied to a simple logging function.

Then I imagined that perhaps Operational Semantics or Hoare Logic could help in "formally proving" the behavior of functions. But the gist of the answers was "it's too hard" or "it's impractical". Nevertheless, it seems that CompCert accomplished it (but not sure if they used Hoare Logic, Operational Semantics, or others), or maybe I am missing something. So what my sense is is there is no use in Hoare Logic or Operational Semantics in practical software development. I would like to be proven wrong on that.

I realize that Model Checking is a good candidate for matching a program model with a specification. But the question still remains, how you know that your model is correct in the first place. That is where it seems formal proofs or some other formal verification technique could shine somehow (which is what this question is about). Wondering how in practice you can apply formal proofs to software development. How to verify that your Model Checking model is correct. It seems the only answer is "formal proofs". But then the question is how. How to apply formal proofs to your model to verify it is correct. I've tried asking questions about it but have had no luck.