We prove the correctness of a two-way sliding window protocol with piggybacking, where the acknowledgements of the latest received data are attached to the next data transmitted back into the channel. The window sizes of both parties are considered to be finite, though they can be different. We show that this protocol is equivalent (branching bisimilar) to a pair of FIFO queues of finite capacities. The protocol is first modeled and manually proved for its correctness in the process algebraic language of μCRL. We use the theorem prover PVS to formalize and mechanically prove the correctness of the protocol. This implies both safety and liveness (under the assumption of fairness).