We present an overview of a soon-to-start FCT-funded project centered on Contract Guided System Development, a software methodology that aims at producing provably correct applications. The methodology integrates specification, design, and verification, based on the concept of contracts. We intend to follow three complementary directions. The first develops a means to prove the correctness of a class with respect to its specification, written in an assertion language that is in turn expressive and easy to master. The second direction builds a formal specification of abstract data types that is effective in driving the identification of the contracts that must be verified by implementing classes. The third produces tools that generate Java interfaces equipped with contracts from ADT specifications, and that generate monitored classes from contract-annotated Java classes.