http://www.tbrk.org
This is an unofficial reimagining of the Archive of Formal Proofs
Loop freedom of the (untimed) AODV routing protocolby Timothy Bourke and Peter Höfner
Mechanization of the Algebra for Wireless Networks (AWN)by Timothy Bourke