Modern Web Service applications encompass multiple distributed interacting components comprising millions of lines of source code. With this complexity, some bugs remain undetected despite extensive testing procedures, and occasionally cause transient system failures. Incorrect failure handling in applications often leads to incomplete or to unintentional request executions. A family of recovery protocols called interaction contracts provides a generic solution to this problem by means of system-integrated data, process, and message recovery for multi-tier applications. The thesis presents a formal specification of the interaction contracts and their verification using Statemate state-and-activity-charts and integrated model checker, respectively. An efficient implementation for Microsoft Internet Explorer and PHP-based Web Services complements the thesis.