It might be fruitful to combine two approaches, like for example VigNAT authors did > The beauty of symbolic execution lies in its ease of use: it enables auto

It might be fruitful to combine two approaches, like for example VigNAT authors did > The beauty of symbolic execution lies in its ease of use: it enables automatic code analysis, hence can be used by developers without verification expertise. The challenge with symbolic execution is its notorious lack of scalability: applying it to real C code typically leads to path explosion. The part of real NF code that typically leads to unmanageable path explosion is the one that manipulates state. Hence, we split NF code into two parts: > A library of data structures that keep all the “difficult” state, which we then formally prove to be correct—this takes time and formal methods expertise, but can be amortized if the library is re-used across multiple NFs. > Stateless code that uses the library, which we automatically and quickly verify using symbolic execution. > The challenge lies in combining the results of these two verification techniques, and for that we developed a technique we call “lazy proofs” https://vignat.github.io/ https://vignat.github.io/