Brittleness, or proof instability, is the problem where small changes to an SMT query cause the SMT solver to either take much longer to return than previously, or fail to return a result at all. Tackling this problem is critical for SMT-based automated program verifiers, such as Dafny or F*, where small changes to the program or tool versions can trigger brittleness and lead to a bad user experience. Recent work provides methods to measure brittleness, determines that the problem is widespread in practice, and proposes automated ways to reduce its occurrence. In this work we present language features for reducing brittleness that the user applies manually which go beyond what the automated methods proposed previously, could achieve. We show on various examples and on code deployed at scale at MajorCloudProvider that applying these techniques is easy for developers and has significant impact.