Klint allows for fast and automated formal verification of network functions (NF), such as a router or a NAT. It works directly on binaries, without the need of special data structures.
It can ensure that a given NF, be it proprietary or not, respects a formal specification. It allows decoupling between NF-providers and network operators, and let the latter validate it before deploying it.

The network functions can be written in any compiled language, as long as it exposes two functions conforming to Klint: a setup method taking care of initialisation, and another method handling a packet, asserting on the transmitted packet.
Klint provides some well-known NF specification to get you started writing your own, and a way to compile with DPDK.