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?