Reading Error Messages
Understanding what the verifier is telling you.
Counterexample Analysis
Using --counterexample to find the failing case.
Strengthening Preconditions
When verification fails because the verifier cannot prove a callee's precondition at a call site, you need to strengthen preconditions to rule out impossible inputs.
Intermediate Assertions
Breaking complex proofs into smaller, provable steps.
Loop Invariant Discovery
Systematic approach to finding the right invariant when verification fails.