Abstract. We present formal and practical foundations for Web service composition framework with composition correctness guarantees. We introduce contractual composition model based on two isomorphic ion models: Contract Definition Language (XML) and abstract machines (formal notation). Composition operators (patterns) are used to perform composition which is then formally verified with respect to properties described in service contracts. We also describe Java-based implementation of the system, concentrated around Sun’s Java Web Services Development Pack (JWSDP). Indexed terms: Web services, composition, correctness, contracts