Verification languages such as Dafny enable powerful proof automation with Satisfiability Modulo Theories (SMT) solvers. However, SMT-based verification is vulnerable to proof instability, where superficial changes to the source program may cause spurious verification failures. In this extended abstract, we discuss our line of work on proof instability. We start by reviewing our methodology to detect instability and a measurement study on five verification query sets generated by Dafny and F*. We then review our finding on how irrelevant SMT query context contributes to instability, along with a pruning algorithm to reduce instability. Finally, we discuss our ongoing work to control the relevant but unstable context. In this line of work, we quantitatively and systematically study the causes and mitigation of instability, and we hope SMT-based verification will eventually reach a point where we can have stable proofs while leveraging powerful automation.