Bind statements inside SystemVerilog are frequently used by simulation-based verification benches to add verification code to RTL design modules, interfaces, or compilation-unit scopes. With bind statements, verification code is separated from RTL design, so design and verification teams can maintain their own files. Under the context of formal verification, bind statements are also heavily used. In addition to common usages, due to the unique nature of formal verification, the bind statements become more powerful. For example, inside formal verification, an assumption can be used to constrain inputs; a snip point is used to cut the driver logic of a signal; a floating net or un-driven signal can be controlled by formal tools the same way as primary inputs. In this paper, the authors will use real-life examples to demonstrate a few innovative uses of bind statements within formal verification.