What is SMTChecker used for in Solidity?

Question

From the solidity docs:

If you use pragma experimental SMTChecker;, then you get additional safety warnings which are obtained by querying an SMT solver. The component does not yet support all features of the Solidity language and likely outputs many warnings. In case it reports unsupported features, the analysis may not be fully sound.

I understand that SMT comes from "Satisfiability Modulo Theory", but could someone explain how does the concept apply to Solidity? Is it some sort of formal verification?

Answer 1

In oversimplified terms, it is a built-in formal verification module for the Solidity compiler.

It essentially converts a program into statements (or more specifically, into problems) and it then tries to prove whether the code can be broken or not by returning a value of true or false (also acknowledged as either being satisfiable/unsatisfiable in terms of SAT theory).

The idea behind the module is to basically catch bugs and prove the correctness of a program at compile-time, modules like this are often present as compiler optimization features because it is a mathematically proven way ensure behavioral consistency with respect to i.e. the translation process from high level to low level code.