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)?

  • 2
    $\begingroup$ This is a very broad question. Perhaps take a look at the SPIN model checker, and on Coq as a theorem prover, both of which are pretty common in use, and see if you can use them directly, or to gain some understanding about the process. $\endgroup$
    – Shaull
    Commented Dec 25, 2019 at 13:06