A design's behaviour as a transition relation: legal steps, a critical state's preimage as its only ways in, composition through a pipeline, and assert versus assume.
Part of Discrete Mathematics for Formal Verification on formal.org.