This repository contains the artifacts for our formal analysis of Karn's Algorithm and the RTO computation defined in RFC6298.
The Python script recreates Fig. 2 from the paper.
The Ivy scripts prove Observations in Sections 2 and 3.
The ACL2s script proves Observations in Section 4.