Why Formal Verification?

• Most of the bugs in the program turn out to be program specific. Static analysis tools miss out on these bugs and often give false positives. Also these tools are not able to understand the meaning of the code.

• Formal verification helps to find rare bugs by finding out violation of the invariants, which are usually very hard to find. These invariants are properties that a system should always hold true.

• It is should be noted that formal verification involves human in the loop, who is responsible to write invariants. So it is not a fully automated process unlike static analysis.

What are Invariants?

• They are properties of a system which should never be changed.

• For example: The whole is the sum of its parts, the assets are equal to or greater than the liabilities (solvency).

Limitations of Formal verification

• Formal verification tools like Certora Prover timeout if the invariant is computationally hard to verify.

• The invariants that you write can turn out to be non-inductive in nature. Non-inductive invariants cannot be proved via formal verification.

Difference between Formal verification & Fuzzing

• Fuzzing analyzes all the test cases step by step. But for formal verification, it just starts with an arbitrary state.

• It can start anywhere and give you a counterexample or a counter test case that violates the property of the system.

Getting your hands buffed up

To get your hands buffed up and get started with smashing bugs, you need to keep the following in in your mind:

• You don't want to dive too deep in code when writing rules.

• You just want to understand the code enough to write rules. Otherwise you would be writing rules for what the contract does instead of what the contract should be doing. You want to prove things that the contract might not necessarily do.

• You want the idealistic version of the contract in your head when writing rules.

• @withRevert rules should be written and used carefully. They should be used for checking the function for cases when there are revert statement in the function. And we want Certora Prover to get to that revert statement.

• Write a require statement only if you are sure it is not a bug. In simpler words the require statements help us to narrow down the possibilities of what the Certora Prover should consider when testing the cases in a rule.

• Usually the statements or invariants which end in "the transaction doesn't revert" logic are hard to write rules for.

• Use the statement with the language of "MUST" to frame the assert statements. That will help to understand and resolve violations.

• f calls all the functions in order to change the required state. For example: Checking "Only I can increase allowance for my tokens"

• f.selector can be used to narrow down and check state changes for specific functions only. This means that other than these functions if the state changes occur contrary to what we believe, it will throw error.

• filter {} block can be used to filter the functions you want to run. For example: Checking "Only appropriate functions can change the allowance for my tokens"

• Strengthen your system enough to make it an inductive statement which the Certora Prover can prove correctly. It’s because it can happen that the invariants that you write are NOT Inductive. This in turn can result in bad results.

• We always want the invariants to be inductive. It is the human element to write an inductive statement.

• For example:

  x := 1;
  y := 2;
      while do {
          assert x is odd
          x := x + y
          y := y + 2
  }
  

  Note that the initialization is arbitrary in an induction in mathematics: p(n), p(n+1) The tool gives counterexample: x = 2, y = 2 and so on

• You need to specify in the invariant that x is odd and y is even. Then by inductive reasoning you can prove that x + y = odd number.

• There is difference between a property being correct and a property being an invariant. A property can be true, but not inductive!

• From the point of view of a smart contract developer, inductiveness also means "preserved by all public functions of the contract".