NetKAT

A network specification and verification language based on Kleene Algebra with Tests

NetKAT is a domain-specific language for specifying and reasoning about packet-forwarding networks, grounded in Kleene Algebra with Tests (KAT). It provides a sound and complete equational theory for reasoning about network behavior, and supports automated verification via symbolic automata algorithms implemented in the KATch tool. Extensions include GKAT (Guarded KAT) for nearly-linear-time verification and StacKAT for infinite-state networks.