The equational theory of Kleene Algebra with Tests (KAT) provides an algebraic framework to manipulate uninterpreted programs along with a PSPACE-complete procedure for deciding program equivalence. One of the most successful applications of the KAT theory is found in NetKAT, which instantiates the KAT metatheory to an interpreted language with primitives that support reasoning about packets in a network. NetKAT has found wide applications in reasoning about network correctness, with original applications to reachability, traffic isolation, and more. The power of KAT lies in its compact, expressive, and elegant signature - it describes a wide array of imperative programming paradigms, in particular ones which support nondeterminism at the level of programs.Recent research has focused on the guarded fragment of KAT, known in the literature as Guarded Kleene Algebra with Tests (GKAT). This fragment of the KAT language trades expressivity for algorithmic performance. In particular, while remaining uninterpreted, guarded KAT programs have deterministic control flow: given a particular state the next action is completely determined, which differs from KAT in that the latter can compose programs non-deterministically. The upshot is that, even though GKAT can only encode a proper subset of valid KAT programs, the accompanying decision procedure for GKAT is nearly linear compared to the exponential worst-case in KAT. Furthermore, the loss of expressivity is mitigated by the fact that GKAT’s control flow corresponds more closely with traditional programming constructs, such as if-then-else and while-loops. Unfortunately, there have not yet been robust instantiations of the abstract GKAT theory in the same spirit as NetKAT for KAT. This is our present purpose: we aim to combine the primitive semantics and language model from NetKAT with the operations and metatheory from (abstract) GKAT. We offer a limited axiomatization for what we call guarded NetKAT (GNetKAT) and prove soundness and partial-completeness over this fragment. As we discover, it is deceptively difficult to adapt GKAT’s uninterpreted theory to an interpreted setting, as the inclusion of extra axioms and commutativity conditions greatly complicates the metatheory. We proceed to develop a coalgebraic decision procedure to verify GNetKAT semantic program equivalence in nearly linear time, similar to but more elementary than that in the original GKAT setting. We conclude with discussion of applications in the vein of NetKAT. It is our hope that a proper understanding of how GKAT instantiates to its concrete models will motivate further developments in GKAT’s theory, in particular towards resolving its non-algebraic axiomatization.