Given that there are examples of formal proofs used to formally verify real-world software applications, I would like to know what these people and teams actually do to create these formal proofs. That is, the kind of code they write and/or the types of formal proofs they create, and how the proofs work. For example, maybe the proofs are term derivation trees, or state-transition graphs, etc.
I understand how model checking works, but the model itself should probably be "proven" somehow even before checking it against a specification. What I am wondering here is only about proofs. For example, in airplanes, what types of things they are proving, and how they are going about proving them. For example, maybe they prove that the plane will land if this button is pressed. That is the what they prove part. Then they do this by writing some Coq code that is exported to ocaml, and in the Coq code they have to prove x about the button itself, and y about the forces of air while the plane is flying, and z that the air brakes will apply effective force etc. And they do this by starting from axioms a b and c. That is the how part.
I don't need to know exactly they are doing the specific proofs, just generally how they go about it. I would like to know generally what they start from, how they formalize and prove it (the model not the spec) in a language, and how this results in a feeling of "now our code is proven". My previous questions about proofs didn't go into enough depth about how the proofs actually work.
Another example from the link is satellite technology, compilers, and os-kernels.
Many system verification papers are very easily accessible.
This is exactly what I mean with elitism. Most system verification papers are extremely difficult to read for people who are not familiar with the matter. Just because something comes easy to you doesn't mean it's easy for others. I came to this question hoping for a good resource/blog post with a good example for a formal proof of verified software, with an understandable explanation. Thus far I haven't been able to find something like this online, and I think this attitude is part of the reason for it. $\endgroup$