Formal verification is a code analysis technique that attempts to exhaustively prove or disprove certain security properties using a solver.

Example tools

• SMTChecker, a Solidity built-in formal verifier
• Manticore

Trade-offs

Pros

• Formal verification can be used to prove certain properties are true and can provide a high degree of confidence
• Formal verification is able to parse the code and figure out how to cover certain branches that can only be accessed by meeting complex conditions

Cons

• Formal verifiers are very slow since they are using a general purpose solver. Beyond the processing cost, formal verification runs are also time consuming to set up and tune
• Formal verification is much easier with a deep understanding of how the underlying solver works

Advanced features

Formal verifiers differ in how they represent data. For example, most cannot deal very well with cryptographic functions, e.g., hashing so a technique is used whereby the hash function is treated as an unknown ("uninterpreted") function. Other formal verifiers struggle with memory representation and can only work with code that accesses fixed memory indices. Unfortunately, working effectively with a formal verifier often requires understanding how it models programs and their specific shortcomings.

Some formal verifiers offer numerous "back-ends" or solver engines. Some solver engines are better at certain types of tasks and worse at others.

When to use formal verification

It's difficult to prescribe formal verification with a specific rule but below are some filters to judge when formal verification could be useful:

• Does the code contain very high security risk (e.g., potential for significant loss of funds)
• Is the core free from external calls (more "pure" components are easier to verify than heavily integrated components)
• Is the arithmetic relatively simple (no multiplications, divisions or modulo operations)
• Is there very limited iteration (ideally no loops and no recursion)

‍