Abstract. Clever algorithm design is sometimes superseded by simple encodings into logic. We apply this motto to a few case studies in the formal verification of security properties. In particular, we examine confidentiality objectives in hardware circuit descriptions written in VHDL.