Design constraints express essential behavioural properties of a software system. Two key elements of a scheme for enforcing design constraints are presented: a logic for describing the constraints, and an analysis that can be used both to explore the constraints in isolation (and thus gain confidence in their correctness), and to check that they are obeyed by an implementation. Examples of applications of the d its analysis at various levels of abstraction are given, from high-level designs to finding bugs in code. The challenge of bridging several levels, and checking code abstract design constraints, is illustrated with a scenario from an air-traffic control system.