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.
Presentation
Technical