We pressent an approach to reasoning about the functional behaviour of circuits. The approach begins and culminates with a technique, Synchronized Transitions, for specifying circuits and culminates with a technique for constructing machine checked proofs that invariants are preserved. We also report on some successful experiments using the approach to verify properties of simple, but nontrivial VLSI circuits.