After an intro to formal methods, it describes examples of hardware, software, and combined verifications of useful protection schemes. Recent work focuses more on HW/SW combined since it provides highest usability, security, and performance combination.