Contract-based design is a useful software engineering paradigm and has been exploited in many literatures for taming the complexity of embedded system development. A system is divided hierarchically into components in a top-down manner, where each component is associated with contracts structured in pairs of assumptions and guarantees. The strength of contract-based design enables stepwise refinement, compositional verification, and reuse of components etc. In this paper, we present a verification framework that builds upon contract-based design to ensure the correctness of embedded software. This framework can be integrated with many formal techniques, e.g., compositional verification, model checking, static analysis, runtime verification, that are shaped in a formal verification chain from the design perspective to the implementation perspective. First, a design level hierarchical model made up of components is abstracted for embedded software, and contracts relevant to components are specified and verified in temporal logic. Second, the behaviour models are constructed for the components located at the bottom of the hierarchical model, and verified using the same contracts at the first step. Third, the implementation of the bottom components are verified, still using the same contracts. Consequently, the consistency between design and implementation of embedded software is strictly proved. We provide a practical case study in the field of aerospace to illustrate the feasibility of our approach, where temporal logic LTL (Linear Temporal Logic) is employed for reasoning as contracts throughout the verification chain.