Model-based software development is a leading methodology for the construction of safety- and mission-critical embedded systems. Formal models of such systems can be validated, via formal verification or testing, against system-level requirements and modified as needed before the actual system is built. In many cases, source code can be even produced automatically from the model once the system designer is satisfied with it. As embedded systems become increasingly large and sophisticated the size and complexity of models grows correspondingly, making the verification of top-level requirements harder, especially in the case of infinite-state systems. We argue that, as with conventional software, contracts are an effective mechanism to establish boundaries between components in a system model, and can be used to aid the verification of system-level properties by using compositional reasoning techniques. Component-level contracts also enable formal analyses that provide more accurate feedback to identify sources of errors or the parts of a system that contribute to the satisfaction of a given requirement. This talk discusses our experience in designing an assume-guarantee-based contract language on top of the Lustre modeling language and leveraging it to extend the Kind 2 model checker with contract-based compositional reasoning techniques.