CAIN-42 CAIN StudioCFVE · Module 1 of 5 · 13 min
SMT solving with Z3
An SMT solver decides whether a logical formula over integers, bit-vectors, arrays and more can be satisfied. Z3 is the most widely used.
To verify a rule, ask the negation: 'is there any input for which the rule fails?'. UNSAT means no such input exists: the rule holds for all inputs. SAT returns a concrete counterexample.
UNKNOWN (often a timeout) means nothing was proven, and must be treated as not proven.
Key points
- Ask for a counterexample.
- UNSAT = proven for all inputs.
- SAT = concrete counterexample.
- UNKNOWN = not proven.
In the CAIN-42 codebase
cain/cain_z3_verifygate.py— Z3 verification gate (UNSAT = proof)
Practice check
Practice 1 · choose one
To prove 'balance never negative', you ask Z3 for…
Practice 2 · true or false