SMT-Based Verification in Flex
Flex supports SMT-based verification, which is a verification technique distinct from testing. The advantage of SMT-based verification is that false-positive results are impossible (or at least extremely unlikely). In practice, just because code performs well under black-box testing (e.g., unit testing or fuzz testing) does not guarantee that the code is safe. This is because it is infeasible to test the code for all possible inputs. SMT-based verification digs into the logic of the code to exhaustively consider every possible input in its analysis.
| Type of Result | SMT-based Verification | Black-box Testing |
|---|---|---|
| False Positive | impossible | possible |
| False Negative | impossible | impossible |
| Unknown | possible | impossible |
How can correctness be proved?
Think back to math class. How would you solve equations like x^2 - x = 6? Would you plug in every possible number for x until you found one that works? Of course not! You manipulate the equation to solve for values of x that satisfy the equation (in this case 3 or -2).
Under the hood, an SMT solver is doing something very similar to what you did in math class. It is attempting to find solutions by manipulating the code as a mathematical expression. In particular, it is solving for parameter values that cause the code to fail. For many programs, "solving for failure" is orders of magnitude faster than attempting to find failures by brute-force.
Think again back to math class, and this time you need to find real-number solutions to the equation x^2 + x + 1 = 0. You may think to use the quadratic formula. The quadratic formula gives you two complex solutions (1+2i, 1-2i) and no real solutions. Real solutions, if they exist, must come from the quadratic formula, so you have proven that there aren't any. It's not that you've tried a bunch of real numbers and none of them worked. There are none to find in the first place!
Once again the SMT solver is doing something very similar. In the process of "solving for failures," it may discover that there can be no failures. Thus, the correctness of the code is proved.
To put this into practice, follow the Writing Flex Contracts tutorial.