- TCP/IP handshake modeled in TLA+ for an environment with multiple clients and a single server.
- Can be exhaustively checked in TLA+ toolbox, which found 2000 distinct states and 13000 states for a system with 4 clients.
- Successfully used to catch bugs in the design stage itself.