Formally verified DIR-24-8 Longest Prefix Match data structure. Done in the context of my bachelor project at DSLAB, EPFL.
The static analysis tool used for verification is a modified version of VeriFast along with Z3 Theorem Prover.
The data structure has been added to the Vigor project library.
This repo only contains the code I produced for my bachelor project and won't compile or verify as is, you'll need to use it in the context of the Vigor project.