Formal Verification (FV) has matured as a verification discipline in the past couple of decades becoming mainstream in industrial design and verification methodologies and processes. This talk will provide an introduction to FV, outline the methodology and execution aspects of its unprecedented use within IBM going from being a specialized activity with a narrow focus to a broad-based use significantly improving design and verification productivity, and overview the technology encapsulated in IBM's state-of-the-art FV tool, RuleBase SixthSense Edition, which is the result of more than a decade of active collaboration between IBM EDA and Research. This tool is extensively used within IBM, and to a limited extent is externally licensed, for sequential equivalence checking and functional verification.