Huginn-TCP includes a trace checker that validates a given trace, which consists of captured network frames, UNIX socket API calls, and changes to the TCP control block. The model encodes non-deterministic choices which are taken by existing TCP/IP implementations. The model is accompanied by an extensive test suite.
Huginn-TCP is based on the 2000-2009 Netsem Network Semantics research project, which was validated against the FreeBSD-4.6, the Linux 2.4.20, and the Windows XP TCP/IP implementation. Huginn-TCP takes advantage of the current HOL4 proof system, which uses PolyML (instead of Moscow ML), and is already 20 times faster on average. The tracing subsystem is being replaced by DTrace (on FreeBSD-11), instead of a sockets wrapper, libpcap slurper, and a kernel ringbuffer. The testing subsystem is being rewritten to accommodate this change. Support for newer TCP features such as delayed ACK, selective ACK, LRO, TSO, are planned.