Stop-and-wait proof

This was the final project of the class Logic and Computation I took during the spring 2021 semester. In this project I proved the resilience of the stop-and-wait protocol (most commonly used in bluebooth, a subset of TCP) to network failures -- showing that the data will never be malformed.

The paper can be viewed here, and the source code can be viewed on GitHub here.