Assume-guarantee reasoning for multi-module hardware. Prove each component correct under assumptions about its environment, then compose the component proofs to establish system-level correctness.
Part of Industrial Practice: Scaling Formal Verification on formal.org.