Last year I looked heavily into Formal Verification, such as automated theorem proving, model checking, type systems, symbolic evaluation, and many others. I probably spent a few weeks or maybe months looking into it. At the time, I felt like I had a decent grasp of how it could be applied, yet still couldn't put my finger on exactly what first steps would be. Today, I have forgotten a significant portion of this stuff, or more specifically of implementation details. I get all the different branches of Formal Verification at a high theoretical classroom level, but I don't get how to apply it to writing real software.
The question here is how I can apply formal verification to a project if it were greenfield and free of constraints (yet at the same time, realistic meaning the problems can be solved within a reasonable amount of time). I'm wondering if one could explain relatively briefly how you would apply any/all Formal Verification techniques to gain that mathematical guarantee that your program matches a specification. How do the hardware people do it? How should it be done in software? Basically...
More specifically, nothing comes to mind other than writing unit/integration tests when it comes to making sure I'm building a super complicated program correctly (like an HTTP server). How could I apply model checking, or typechecking, or other things, to my advantage in terms of proofs / guarantees of program correctness (with regards to the specification)?
