How to be good in formal verification?

Using Coq
1

Today I don’t believe in software. Errors are easy to do. When I write code, I have error. I feel that I am not a reliable coder.

To avoid that, I decide to learn formal verification. I start with the lessons on the Software Foundations website. I can understand the content of the lesson. It is theoretical but practical. Still, I think I’m not good in that yet.

Every time I try the theorem, I have to think. I think very hard. If for everything I need to write I have to think so much, my speed to write the code is slow. You can never reach the speed of writing code in normal languages. Because of this, the truth is that I need to improve my speed of thinking more to write faster. I want to hear about the practice tips to improve my speed and competences in formal verification. Any advice?

2

There is no single canonical answer here, some standard answers I’ve heard:

  • Work through exercises in books and other course material.
  • Read the scientific literature to become familiar with techniques and tools, in particular surveys.
  • Do online code challenges.
  • Contribute to open source verification projects (practical training with hard constraints).
  • Enroll in relevant university courses or educational program (master’s/PhD level)
3

The challenge is two-fold: to write a theorem and to prove it.

When playing with the textbook, in most cases the theorem is provided, and your task is to prove it. It’s OK to type Coq tactics mindlessly, but if you’re stuck for 5 minutes, leave the keyboard and write the proof with pen and paper. Coq is an assistant; you are the prover. Ask yourself: What does a mathematical proof for the theorem look like?

Beyond the textbook, your task is to first write the theorems and then prove them. Crafting the theorem is way more challenging. Ask yourself: (1) What do I want to verify? (2) How do I formalize it? and then (3) Is my formalization convenient to verify (via formal proof or rigorous tests)?

Real-world formal verification requires intuitions of abstraction. In addition to working on the SF exercises, try learning how the textbook takes concrete problems and provide abstract views for them.

4

For completeness, I think it should be added that the challenge is often three-fold, with the final challenge being to validate that the proved theorem is really the right one to prove.

To take my favorite example, if you prove a regular expression matcher correct against a specification of regular expressions that is wrong (or a definition of regular language that is wrong), then the theorem may be true, but it’s not of much use to people who want to use a proper regular expression matcher.

Validation can range from connecting your specification to other validated specifications (“reduction”) to more practical experiments involving real-world artifacts (external benchmarks, datasets, etc.).